fact: CoInductive SomeInf (A:Type):(LTree A)->Prop := InfLeft : forall (a:A)(t1 t2:LTree A), SomeInf t1 -> SomeInf (LBin a t1 t2) | InfRight : forall (a:A)(t1 t2:LTree A), SomeInf t2 -> SomeInf (LBin a t1 t2).
imports: Ltree building graft