proposition: Lemma rel_image_maximal_bisimulation_inversion: forall fw1 fw2, rel_image_lift_F_ _ _ bisimilar fw1 fw2 -> maximal_bisimulation (Build_F_coalgebra (F_ w.(states)) (lift_F_ _ _ w.(transition))) (Build_F_coalgebra (F_ w.(states)) (lift_F_ _ _ w.(transition))) fw1 fw2.
proof: Proof. intros fw1 fw2 (x & y & hyp1 & hyp2 & hyp3). subst fw1 fw2; trivial; apply destructor_morphism; trivial. Qed.
imports: Bisimulation