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