proposition: Theorem trans_bisimilar : forall S0 s1 s2 s3, maximal_bisimulation S0 S0 s1 s2 -> maximal_bisimulation S0 S0 s2 s3 -> maximal_bisimulation S0 S0 s1 s3.
proof: Proof. intros S0 s1 s2 s3 hyp12 hyp23. generalize (maximal_bisimulation_is_maximal S0 S0). unfold is_maximal_F_bisimulation. intros [[hyp1 _] hyp2]. apply (hyp2 (fun x =>(fun z=>{ y | maximal_bisimulation S0 S0 x y/\maximal_bisimulation S0 S0 y z}))). assert (a:=comp_is_F_bisimulation_strong S0 S0 S0 (maximal_bisimulation S0 S0) (maximal_bisimulation S0 S0) hyp1 hyp1). exists a; trivial. exists s2; split; trivial. Qed.
imports: ExtensionalFunctor Setoid