proposition: Lemma maximal_bisimulation_is_bisimulation: forall (S1 S2:F_coalgebra), is_F_bisimulation _ _ (maximal_bisimulation S1 S2).
proof: Proof. intros S1 S2. exists (fun s1s2h=> (hd_ _ (fst (proj1_sig s1s2h)), maximal_bisimulation_Str_tl S1 S2 s1s2h)). generalize S1 S2. intros [X_st X_tr] [Y_st Y_tr] [[x y] [hyp_hd hyp_tl]]. simpl; split; rewrite surjective_pairing; trivial. simpl in hyp_hd; rewrite hyp_hd; trivial. Defined.
imports: WeaklyFinalCoalgebra