fact: Definition maximal_bisimulation_conat_pred : forall (S1 S2:F_coalgebra), {s1s2 : S1.(states) * S2.(states)| maximal_bisimulation _ _ (fst s1s2) (snd s1s2)} -> unit + {s1s2 : S1.(states) * S2.(states)| maximal_bisimulation _ _ (fst s1s2) (snd s1s2)}.
imports: WeaklyFinalCoalgebra