fact: Definition is_lambda_bisimulation_strong (S1 S2:TB_bialgebra) (slR: states (S1.(coalgebra_part)) -> states (S2.(coalgebra_part)) -> Set) := { gamma : {s1s2 : states (coalgebra_part S1) * states (coalgebra_part S2) & slR (fst s1s2) (snd s1s2)} -> B_ (T_ {s1s2 : states (coalgebra_part S1) * states (coalgebra_part S2) & slR (fst s1s2) (snd s1s2)}) | forall (s1s2h:{s1s2 : states (coalgebra_part S1) * states (coalgebra_part S2) & slR (fst s1s2) (snd s1s2)}), (lift_B_ _ _ (fun fr=>S1.(algebra_part)(lift_T_ {s1s2 : states (coalgebra_part S1) * states (coalgebra_part S2) & slR (fst s1s2) (snd s1s2)} _ (fun s1s2h_=>fst (projT1 s1s2h_)) fr ) ) (gamma s1s2h) = transition S1.(coalgebra_part) (fst (projT1 s1s2h))) /\ (lift_B_ _ _ (fun fr=>S2.(algebra_part)(lift_T_ {s1s2 : states (coalgebra_part S1) * states (coalgebra_part S2) & slR (fst s1s2) (snd s1s2)} _ (fun s1s2h_=>snd (projT1 s1s2h_)) fr ) ) (gamma s1s2h) = transition S2.(coalgebra_part) (snd (projT1 s1s2h))) }.
imports: LambdaCoiteration