proposition: Theorem LTree_bisimilar_label : forall (p:path) (t t': LTree A), LTree_bisimilar t t' -> LTree_label t p = LTree_label t' p.
proof: Proof. simple induction p. intros t t'; case t, t'. - reflexivity. - inversion_clear 1. - inversion_clear 1. - inversion_clear 1; simpl; auto. - intros a l;case a; intros H t t'; case t, t'. + reflexivity. + inversion_clear 1. + inversion_clear 1. + inversion_clear 1; cbn; repeat rewrite LTree_label_rw0; auto. + repeat rewrite LTree_label_rw1; auto. + inversion_clear 1. + inversion_clear 1. + inversion_clear 1; repeat rewrite LTree_label_rw1; auto. Qed.
imports: Tree_Inf RelationClasses