proposition: Lemma F_unfold_morphism (S0:F_coalgebra) x y : (maximal_bisimulation S0 S0) x y -> (F_unfold S0) x (=) (F_unfold S0) y.
proof: Proof. intros hyp1; apply (F_unfold_bisim_congruence _ (maximal_bisimulation S0 S0)); trivial; apply maximal_bisimulation_is_bisimulation. Qed.
imports: Bisimulation