proposition: Theorem label_LTree_bisimilar : forall t t': LTree A, (forall p:path, LTree_label t p = LTree_label t' p)-> LTree_bisimilar t t'.
proof: Proof. cofix label_LTree_bisimilar. intros t t'; case t; case t'. - left. - intros a l l0 H; discriminate (H nil). - intros a l l0 H; discriminate (H nil). - intros a l l0 a0 t1 t2 H. assert (e : a = a0) by (generalize (H nil); injection 1; congruence). subst a0; constructor; apply label_LTree_bisimilar; intro p. + generalize (H (cons d0 p));repeat rewrite LTree_label_rw0; auto. + generalize (H (cons d1 p)); repeat rewrite LTree_label_rw1; auto. Qed.
imports: Tree_Inf RelationClasses