proposition: Lemma inv_is_F_bisimulation (S1 S2:F_coalgebra) (R:S1.(states)->S2.(states)->Prop): is_F_bisimulation _ _ R -> is_F_bisimulation _ _ (fun x=>(fun y=>R y x)).
proof: Proof. intros [gamma gamma_prop]. set (RS21:={s2s1 : states S2 * states S1 | R (snd s2s1) (fst s2s1)}). set (RS12:={s1s2 : states S1 * states S2 | R (fst s1s2) (snd s1s2)}). set (i:=fun s1s2h:RS12=>(exist (fun z=>R (snd z) (fst z)) (snd (proj1_sig s1s2h),fst (proj1_sig s1s2h)) (proj2_sig s1s2h))). set (i_inv:=fun s2s1h:RS21=>(exist (fun z=>R (fst z) (snd z)) (snd (proj1_sig s2s1h),fst (proj1_sig s2s1h)) (proj2_sig s2s1h))). exists (fun s2s1h => lift_F_ _ _ i (gamma (i_inv s2s1h)):F_ RS21). intros s1s2h. generalize (gamma_prop (i_inv s1s2h)). destruct s1s2h as [[s1 s2] hyp]. simpl in hyp. simpl; intros [g_p1 g_p2]; split; simpl; rewrite lift_F_compose; [ rewrite <- g_p2 | rewrite <- g_p1 ]; trivial. Defined.
imports: ExtensionalFunctor Setoid