proposition: Lemma Not_SomeFin_EveryInf : forall (A:Type)(t: LTree A), ~ SomeFin t -> EveryInf t.
proof: Proof. intros A ; cofix H. intro t; destruct t as [| a t1 t2]. - destruct 1; constructor. - intro H0; split ; apply H; red; auto. Qed.
imports: Ltree building graft