proposition: Lemma destructor_equal_inversion: forall x1 x2, w.(transition) x1 = w.(transition) x2 -> x1 (=) x2.
proof: Proof. intros x1 x2 hyp1. rewrite <- (coconstructor_destructor x1). rewrite <- (coconstructor_destructor x2). apply F_unfold_morphism. rewrite hyp1. apply refl_bisimilar. Qed.
imports: Bisimulation