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'. set (hyp:=projT2 h_coind). set (gamma:=projT1 h_coind). set (s1s2h:=existS (fun s1s2=> R' (fst s1s2) (snd s1s2)) (s1,s2) hyp'). destruct (hyp s1s2h) as [hyp1 hyp2]. clear hyp. unfold lift_F_ in hyp1,hyp2; simpl in hyp1, hyp2. change (match gamma s1s2h with | inl star => inl X star | inr x => inr unit (fst (projT1 x)) end = X_tr s1) in hyp1. change (match gamma s1s2h with | inl star => inl Y star | inr x => inr unit (snd (projT1 x)) end = Y_tr s2) in hyp2. destruct (gamma s1s2h) as [u|[[s1' s2'] hyp]]. constructor 1; unfold states, transition; [rewrite <- hyp1 |rewrite <- hyp2] ; f_equal; destruct u; reflexivity. constructor 2 with s1' s2';unfold states, transition; [rewrite <- hyp1 |rewrite <- hyp2| ]; [f_equal|f_equal|]. apply (maximal_bisimulation_is_maximal _ _ R' h_coind); assumption. Qed.
imports: WeaklyFinalCoalgebra