proposition: Theorem refl_bisimilar : forall S0 s, maximal_bisimulation S0 S0 s s.
proof: Proof. intros S0 s. generalize (maximal_bisimulation_is_maximal S0 S0). unfold is_maximal_F_bisimulation. intros [hyp1 hyp2]. apply (hyp2 (@eq S0.(states))); trivial. assert (a:=delta_is_F_bisimulation S0). exists (is_F_bisimulation_is_F_bisimulation_strong _ _ (@eq S0.(states)) a); trivial. Qed.
imports: ExtensionalFunctor Setoid