proposition: Lemma F_unfold_bisim_congruence (S0:F_coalgebra) R x y : (is_F_bisimulation S0 S0 R) -> R x y -> (F_unfold S0) x (=) (F_unfold S0) y.
proof: Proof. intros [gamma hyp_gamma] hyp1. change ( (fun s1s2 => F_unfold S0 (fst (proj1_sig s1s2))) (exist (fun s1s2=> R (fst s1s2) (snd s1s2)) (x,y) hyp1) (=) (fun s1s2 => F_unfold S0 (snd (proj1_sig s1s2))) (exist (fun s1s2=> R (fst s1s2) (snd s1s2)) (x,y) hyp1) ). apply (F_unique (Build_F_coalgebra {s1s2 : states S0 * states S0 | R (fst s1s2) (snd s1s2)} gamma)); intros s1s2hyp; destruct (hyp_gamma s1s2hyp) as [H1 H2]; [ rewrite (commutativity_F_unfold S0 (fst (proj1_sig s1s2hyp))); rewrite <- H1 | rewrite (commutativity_F_unfold S0 (snd (proj1_sig s1s2hyp))); rewrite <- H2] ; rewrite lift_F_compose; apply lift_F_extensionality; trivial. Qed.
imports: Bisimulation