From ffc792ee022360d58969b78e00a90681be1013e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 09:59:48 -0800
Subject: [PATCH] test: dep-elim `cases`

---
 tests/lean/run/induction1.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index 114bd9c738..3a74c5fb69 100644
--- a/tests/lean/run/induction1.lean
+++ b/tests/lean/run/induction1.lean
@@ -114,3 +114,15 @@ theorem tst14 (x : Tree) (h : x = Tree.leaf₁) : x.isLeaf₁ = true := by
   induction x
   | leaf₁ => rfl
   | _     => injection h
+
+inductive Vec (α : Type) : Nat → Type
+  | nil  : Vec α 0
+  | cons : (a : α) → {n : Nat} → (as : Vec α n) → Vec α (n+1)
+
+def getHeads {α β} {n} (xs : Vec α (n+1)) (ys : Vec β (n+1)) : α × β := by
+  cases xs
+  cases ys
+  apply Prod.mk
+  assumption
+  assumption
+  done