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