proposition: Lemma maximal_bisimulation_is_maximal:forall (S1 S2:F_coalgebra), is_maximal_F_bisimulation _ _ (maximal_bisimulation S1 S2).
proof: Proof. intros S1 S2. split. exists (maximal_bisimulation_is_bisimulation S1 S2); trivial. intros R' [hyp_R' _]. revert S1 S2 R' hyp_R'. cofix. intros [X X_tr] [Y Y_tr] R' h_coind s1 s2 hyp'. constructor. destruct h_coind as [gamma hyp]. set (s1s2h:=existS (fun s1s2=> R' (fst s1s2) (snd s1s2)) (s1,s2) hyp'). destruct (hyp s1s2h) as [hyp1 hyp2]. clear hyp. unfold F_ in gamma. unfold lift_F_ in hyp1,hyp2; simpl in hyp1, hyp2. unfold hd_. rewrite <- hyp1. rewrite <- hyp2. destruct (gamma s1s2h); trivial. apply (maximal_bisimulation_is_maximal _ _ R' h_coind). destruct h_coind as [gamma hyp]. set (s1s2h:=existS (fun s1s2=> R' (fst s1s2) (snd s1s2)) (s1,s2) hyp'). destruct (hyp s1s2h) as [hyp1 hyp2]. clear hyp. unfold F_ in gamma. unfold lift_F_ in hyp1,hyp2; simpl in hyp1, hyp2. unfold tl_. set (gam_s1s2h:=gamma s1s2h). set (xyh:=snd (gam_s1s2h)). set (b0:=fst (gam_s1s2h)). assert (hyp1_1:(b0,fst (projT1 xyh))=X_tr s1); [rewrite <- hyp1; subst xyh gam_s1s2h; destruct (gamma s1s2h); trivial|]. assert (hyp2_1:(b0,snd (projT1 xyh))=Y_tr s2); [rewrite <- hyp2; subst xyh gam_s1s2h; destruct (gamma s1s2h); trivial|]. rewrite <- hyp1_1. rewrite <- hyp2_1. destruct xyh as [[x y] h]. trivial. Qed.
imports: WeaklyFinalCoalgebra