fact: Definition bisim_pullback_structure (S1 S2 S3:F_coalgebra) R12 R23 (hyp1 : is_F_bisimulation S1 S2 R12) (hyp2 : is_F_bisimulation S2 S3 R23) (x : weak_pullback_Rel S1 S2 S3 R12 R23) := wkpk_id_rht _ _ _ _ _ (let RS12 := {s1s2 : states S1 * states S2 | R12 (fst s1s2) (snd s1s2)} in let RS23 := {s2s3 : states S2 * states S3 | R23 (fst s2s3) (snd s2s3)} in let r2 := fun r : RS12 => snd (proj1_sig r) in let r3 := fun r : RS23 => fst (proj1_sig r) in pre_bisim_pullback_structure S1 S2 S3 R12 R23 hyp1 hyp2 x).
imports: ExtensionalFunctor Setoid