proposition: Lemma Finite_Not_SomeInf : forall (A:Type) (t: LTree A), Finite t -> ~ SomeInf t.
proof: Proof. intros A t H; induction H as [| a t1 t2 H1 IHt1 H2 IHt2]. - red; inversion 1. - inversion 1; tauto. Qed.
imports: Ltree building graft