proposition: Remark Not_Finite_or : forall (A:Type) (a:A) (t1 t2: LTree A), ~ Finite (LBin a t1 t2) -> ~ Finite t1 \/ ~Finite t2.
proof: Proof. intros A a t1 t2 H; apply demorgan; intro; apply H. right; apply class; tauto. Qed.
imports: Ltree building graft