proposition: Lemma bisimulation_strong_maximal_bisimulation:forall (S1 S2:F_coalgebra) (R:S1.(states)->S2.(states)->Set) x y, R x y-> is_F_bisimulation_strong _ _ R -> maximal_bisimulation S1 S2 x y.
proof: Proof. intros S1 S2 R x y hyp_R hyp_bisim. destruct (maximal_bisimulation_is_maximal S1 S2) as [hyp1 hyp2]. apply (hyp2 R); trivial; exists hyp_bisim; trivial. Qed.
imports: ExtensionalFunctor Setoid