fact: Definition is_maximal_F_bisimulation (S1 S2:F_coalgebra) (R:S1.(states) -> S2.(states) -> Prop) := (exists a:is_F_bisimulation S1 S2 R, True) /\ forall R', (exists a:is_F_bisimulation_strong S1 S2 R',True) -> forall s1 s2, R' s1 s2 -> R s1 s2.
imports: ExtensionalFunctor Setoid