simp [BTree.graft, ih_l, ih_r]
case node
α : Type
u v : BTree α
a : α
l r : BTree α
ih_l : graft (graft l u) v = graft l (graft u v)
ih_r : graft (graft r u) v = graft r (graft u v)
⊢ graft (graft (node a l r) u) v = graft (node a l r) (graft u v)
no goals