From e9748dd0f9cd825d88621f63009696bb6c66e559 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Aug 2020 13:35:16 -0700
Subject: [PATCH] test: match equality proofs

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

diff --git a/tests/lean/match3.lean b/tests/lean/match3.lean
index e686a998d8..e503022776 100644
--- a/tests/lean/match3.lean
+++ b/tests/lean/match3.lean
@@ -38,3 +38,13 @@ begin
   subst h₁;
   assumption
 end
+
+theorem ex7 (a : Bool) (p q : Prop) (h₁ : a = true → p) (h₂ : a = false → q) : p ∨ q :=
+match h:a with
+| true  => Or.inl $ h₁ h
+| false => Or.inr $ h₂ h
+
+def head {α} (xs : List α) (h : xs = [] → False) : α :=
+match he:xs with
+| []   => False.elim $ h he
+| x::_ => x