proposition: Lemma stepl_bisimilar : forall S0 s1 s2 s3, maximal_bisimulation S0 S0 s1 s2 -> s1 = s3 -> maximal_bisimulation S0 S0 s3 s2.
proof: Proof. intros S0 s1 s2 s3 hyp12 hyp13; subst s1; assumption. Qed.
imports: ExtensionalFunctor Setoid