Theorem: LoVe.BTree.map_eq_empty_iff (LoVe/Labs/Lab5Solution.lean)

State before:
α β : Type
f : α → β
⊢ map f empty = empty ↔ empty = empty
Tactic:
simp [BTree.map]
State after:
no goals

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