proposition: Lemma image_span_is_F_bisimulation_strong : forall (S1 S2 S3:F_coalgebra) (f:S2.(states)->S1.(states)) (g:S2.(states)->S3.(states)), (forall s2, lift_F_ _ _ f (S2.(transition) s2) = S1.(transition) (f s2)) -> (forall s2, lift_F_ _ _ g (S2.(transition) s2) = S3.(transition) (g s2)) -> is_F_bisimulation_strong S1 S3 (fun x=>(fun y=>{s2:S2.(states) | f s2 = x /\ g s2= y} )).
proof: Proof. intros [S1 alpha_1] [S2 alpha_2] [S3 alpha_3] f g hyp_f hyp_g. set (R:=fun x y => {s2:S2 | f s2 = x /\ g s2= y}). set (R13 := {s1s3 : S1 * S3 & R (fst s1s3) (snd s1s3)}). set (i:=fun (is1 : R13) => proj1_sig (projT2 is1)). set (j:=fun s2:S2 => existT (fun s1s3 : S1 * S3 => R (fst s1s3) (snd s1s3)) (f s2, g s2) (exist (fun s2' : S2 => f s2' = fst (f s2, g s2) /\ g s2' = snd (f s2, g s2)) s2 (conj (refl_equal (fst (f s2, g s2))) (refl_equal (snd (f s2, g s2))))) ). exists (fun is:R13 => lift_F_ _ _ j (alpha_2 (i is))). intros [[s1 s3] [s2 [hyp1 hyp2]]]. simpl in *. do 2 rewrite lift_F_compose. split; [ stepr (alpha_1 (f s2)); [rewrite <- hyp_f|subst s1; trivial] | stepr (alpha_3 (g s2)); [rewrite <- hyp_g|subst s3; trivial] ]; subst i; apply lift_F_extensionality; trivial. Qed.
imports: ExtensionalFunctor Setoid