proposition: Theorem sym_bisimilar : forall S0 s1 s2, maximal_bisimulation S0 S0 s1 s2 -> maximal_bisimulation S0 S0 s2 s1.
proof: Proof. intros S0 s1 s2 hyp. generalize (maximal_bisimulation_is_maximal S0 S0). unfold is_maximal_F_bisimulation. intros [[hyp1 _] hyp2]. apply (hyp2 (fun x =>(fun y=>maximal_bisimulation S0 S0 y x))); trivial. assert (a:=inv_is_F_bisimulation S0 S0 (maximal_bisimulation S0 S0) hyp1). exists (is_F_bisimulation_is_F_bisimulation_strong _ _ _ a); trivial. Qed.
imports: ExtensionalFunctor Setoid