proposition: Lemma effobs12_commute : forall A1 A2 c1 c2, commute (θ1 A1 c1) (θ2 A2 c2).
proof: Proof. move=> A1 A2 c1 c2. unfold commute. rewrite /commute -releffobs_eq_effobs1 -releffobs_eq_effobs2. reflexivity. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)