From 93cc8a6403267857ca7af5d4ab810b4b562a4fa1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 27 Nov 2020 09:00:11 -0800
Subject: [PATCH] chore: fix test

It was working for the wrong reasons
---
 tests/lean/run/subst1.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/tests/lean/run/subst1.lean b/tests/lean/run/subst1.lean
index 393f2d8dcd..9103ddb92d 100644
--- a/tests/lean/run/subst1.lean
+++ b/tests/lean/run/subst1.lean
@@ -1,4 +1,4 @@
-
+--
 
 set_option trace.Meta.Tactic.subst true
 
@@ -14,13 +14,12 @@ theorem tst2 (x y z : Nat) : y = z → x = z + y → x = z + z := by
   subst h2
   exact rfl
 
-def BV (n : Nat) : Type := Unit
+def BV (n : Nat) : Type := { a : Array Bool // a.size = n }
 
-theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1) w := by
+theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by
 subst h1
 apply h2
 
-
 theorem tst4 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by
 subst n
 apply h2