proposition: Lemma pre_bisim_pullback_structure_prop1 (S1 S2 S3:F_coalgebra) R12 R23 (hyp1:is_F_bisimulation _ _ R12) (hyp2:is_F_bisimulation _ _ R23) (x:weak_pullback_Rel S1 S2 S3 R12 R23): proj1_sig hyp1 (fst (proj1_sig x)) = fst (proj1_sig (pre_bisim_pullback_structure _ _ _ _ _ hyp1 hyp2 x)).
proof: Proof. destruct hyp1 as [gamma1 hyp1], hyp2 as [gamma2 hyp2], x as [[ [[s1 s2] hyp12] [[s2' s3] hyp23]] hyp]; trivial. Qed.
imports: ExtensionalFunctor Setoid