proposition: Lemma graft_unfold2 {A: Type}: forall (a:A) (t1 t2 t':LTree A), (graft (LBin a t1 t2) t')= (LBin a (graft t1 t') (graft t2 t')).
proof: Proof. intros a t1 t2 t'; LTree_unfold (graft (LBin a t1 t2) t'); simpl; auto. Qed.
imports: Ltree