proposition: Lemma graft_unfold {A: Type}: forall (t t': LTree A), graft t t' = match t with | LLeaf => t' | LBin n t1 t2 => LBin n (graft t1 t') (graft t2 t') end.
proof: Proof. intros t t'; case t. - apply graft_unfold1. - intros; apply graft_unfold2. Qed.
imports: Ltree