proposition: Theorem graft_Finite_LLeaf : forall (A:Type) (t: LTree A), Finite t -> graft t LLeaf = t.
proof: Proof. intros A t H; induction H as [| a t1 t2 H1 IHt1 H2 IHt2]. - rewrite graft_unfold; auto. - rewrite graft_unfold, IHt1, IHt2; auto. Qed.
imports: Ltree building graft