Theorem: LoVe.FullBTree.mirror_mirror (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
α : Type
t : FullBTree α
⊢ mirror (mirror t) = t
Tactic:
apply Subtype.eq
State after:
case a
α : Type
t : FullBTree α
⊢ ↑(mirror (mirror t)) = ↑t

State before:
case a
α : Type
t : FullBTree α
⊢ ↑(mirror (mirror t)) = ↑t
Tactic:
simp [FullBTree.mirror, LoVe.mirror_mirror]
State after:
no goals