From 34d98790616f1ff895dc75d32eacbf0bb210fa9c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Aug 2020 13:14:16 -0700
Subject: [PATCH] test: add new tests

---
 tests/lean/match3.lean | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/tests/lean/match3.lean b/tests/lean/match3.lean
index ed3f7685a3..e686a998d8 100644
--- a/tests/lean/match3.lean
+++ b/tests/lean/match3.lean
@@ -9,3 +9,32 @@ match x with
 #eval f 20
 #eval f 0
 #eval f 30
+
+
+universes u
+
+theorem ex1 {α : Sort u} {a b : α} (h : a ≅ b) : a = b :=
+match α, a, b, h with
+| _, _, _, HEq.refl _ => rfl
+
+theorem ex2 {α : Sort u} {a b : α} (h : a ≅ b) : a = b :=
+match a, b, h with
+| _, _, HEq.refl _ => rfl
+
+theorem ex3 {α : Sort u} {a b : α} (h : a ≅ b) : a = b :=
+match b, h with
+| _, HEq.refl _ => rfl
+
+theorem ex4  {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
+match β, a', b, h₁, h₂ with
+| _, _, _, rfl, HEq.refl _ => HEq.refl _
+
+theorem ex5  {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
+match a', h₁, h₂ with
+| _, rfl, h₂ => h₂
+
+theorem ex6  {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
+begin
+  subst h₁;
+  assumption
+end