Theorem: LoVe.BTree.graft_empty (LoVe/Labs/Lab7Solution.lean)

State before:
α : Type
t : BTree α
⊢ graft t empty = t
Tactic:
induction t with
| empty                => rfl
| node a l r ih_l ih_r => simp [BTree.graft, ih_l, ih_r]
State after:
no goals

State before:
case empty
α : Type
⊢ graft empty empty = empty
Tactic:
rfl
State after:
no goals

State before:
case node
α : Type
a : α
l r : BTree α
ih_l : graft l empty = l
ih_r : graft r empty = r
⊢ graft (node a l r) empty = node a l r
Tactic:
simp [BTree.graft, ih_l, ih_r]
State after:
no goals