fact: CoInductive LTree_bisimilar : LTree A -> LTree A -> Prop := LTree_bisimilar_leaf : LTree_bisimilar LLeaf LLeaf | LTree_bisimilar_bin : forall (a:A) (t1 t'1 t2 t'2 : LTree A), LTree_bisimilar t1 t'1 -> LTree_bisimilar t2 t'2 -> LTree_bisimilar (LBin a t1 t2) (LBin a t'1 t'2).
imports: Tree_Inf RelationClasses