proposition: Lemma is_F_bisimulation_strong_Prop_is_F_bisimulation (S1 S2:F_coalgebra) (R:S1.(states)->S2.(states)->Prop): is_F_bisimulation_strong _ _ R -> is_F_bisimulation _ _ R.
proof: Proof. intros [gamma hyp]. set (RS12:={s1s2 : states S1 * states S2 | R (fst s1s2) (snd s1s2)}). set (RS12_:={s1s2 : states S1 * states S2 & R (fst s1s2) (snd s1s2)}). set (id_:=fun s1s2h:RS12=> existS (fun z=>R (fst z) (snd z)) (fst (proj1_sig s1s2h),snd (proj1_sig s1s2h)) (proj2_sig s1s2h):RS12_). set (id__:=fun s1s2h:RS12_=> exist (fun z=>R (fst z) (snd z)) (fst (projT1 s1s2h),snd (projT1 s1s2h)) (projT2 s1s2h):RS12). exists (fun s2s1h => lift_F_ _ _ id__ (gamma (id_ s2s1h)):F_ RS12). intros s1s2_h. destruct (hyp (sigT_of_sig s1s2_h)) as [hyp1 hyp2]. destruct s1s2_h as [[s1 s2] hypR]. split; simpl; simpl in hyp1, hyp2; [rewrite <- hyp1 |rewrite <- hyp2]; rewrite lift_F_compose; apply lift_F_extensionality; intros [[x1 x2] hx]; trivial. Defined.
imports: ExtensionalFunctor Setoid