proposition: Lemma destructor_maximum_bisimulation_inversion: forall x1 x2, maximal_bisimulation (Build_F_coalgebra (F_ w.(states)) (lift_F_ _ _ w.(transition))) (Build_F_coalgebra (F_ w.(states)) (lift_F_ _ _ w.(transition))) (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; assumption. Qed.
imports: Bisimulation