rw [Eq_from_Heq j i]
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
case h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq j i