proposition: Lemma relation_equivalence_bisimulation (S1 S2:F_coalgebra) (R0 R1:S1.(states)->S2.(states)->Prop): is_F_bisimulation _ _ R0 -> (forall x y, R1 x y <-> R0 x y) -> is_F_bisimulation _ _ R1.
proof: Proof. intros [gamma0 hyp_gamma0] hypsub. assert (hypsub1:= fun x y=> match hypsub x y with | conj H0 _ => H0 end). assert (hypsub2:= fun x y=> match hypsub x y with | conj _ H1 => H1 end). red. set (R0_:={s1s2 : states S1 * states S2 | R0 (fst s1s2) (snd s1s2)}). set (R1_:={s1s2 : states S1 * states S2 | R1 (fst s1s2) (snd s1s2)}). set (i10:= (fun (s0s1h:R1_) => exist (fun s1s2=> R0 (fst s1s2) (snd s1s2)) (fst (proj1_sig s0s1h), snd (proj1_sig s0s1h)) (hypsub1 (fst (proj1_sig s0s1h)) (snd (proj1_sig s0s1h)) (proj2_sig s0s1h))) : R1_ -> R0_). set (i01:= (fun (s0s1h:R0_) => exist (fun s1s2=> R1 (fst s1s2) (snd s1s2)) (fst (proj1_sig s0s1h), snd (proj1_sig s0s1h)) (hypsub2 (fst (proj1_sig s0s1h)) (snd (proj1_sig s0s1h)) (proj2_sig s0s1h))) : R0_ -> R1_). exists (fun r1_=> lift_F_ _ _ i01 (gamma0 (i10 r1_))). intros s1s2h. generalize (hyp_gamma0 (i10 s1s2h)). clear. fold R0_. do 2 rewrite lift_F_compose. auto. Qed.
imports: ExtensionalFunctor Setoid