Theorem: LoVe.mirror_Eq_empty_Iff (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
α : Type
⊢ mirror BTree.empty = BTree.empty ↔ BTree.empty = BTree.empty
Tactic:
simp [mirror]
State after:
no goals

State before:
α : Type
a✝² : α
a✝¹ a✝ : BTree α
⊢ mirror (BTree.node a✝² a✝¹ a✝) = BTree.empty ↔ BTree.node a✝² a✝¹ a✝ = BTree.empty
Tactic:
simp [mirror]
State after:
no goals