fact: Definition is_F_bisimulation_strong (S1 S2:F_coalgebra) (R:S1.(states) -> S2.(states) -> Set) := { gamma : {s1s2 : states S1 * states S2 & R (fst s1s2) (snd s1s2)} -> F_ {s1s2 : states S1 * states S2 & R (fst s1s2) (snd s1s2)} & forall (s1s2_h:{s1s2 : states S1 * states S2 & R (fst s1s2) (snd s1s2)}), lift_F_ _ _ (fun z : { z : states _ * states _ & R (fst z) (snd z) }=>fst(projT1 z)) (gamma s1s2_h)=S1.(transition) (fst(projT1 s1s2_h)) /\ lift_F_ _ _ (fun z : { z : states _ * states _ & R (fst z) (snd z) }=>snd(projT1 z)) (gamma s1s2_h)=S2.(transition) (snd(projT1 s1s2_h))}.
imports: ExtensionalFunctor Setoid