proposition: Lemma F_unfold_morphism_inversion (S0:F_coalgebra) x y : (F_unfold S0) x (=) (F_unfold S0) y -> (maximal_bisimulation S0 S0) x y.
proof: Proof. intros hyp1. set (f:=F_unfold S0). set (f_inv_delta:=fun x y=> f x (=) f y). apply bisimulation_maximal_bisimulation with f_inv_delta. assumption. apply inverse_image_F_bisimulation_is_F_bisimulation with (S2 := w). subst f; intros s0; symmetry; apply (commutativity_F_unfold S0 s0). apply maximal_bisimulation_is_bisimulation. Qed.
imports: Bisimulation