proposition: Lemma fromFreeCommute A1 A2 : forall c1 c2, commute (θ1 A1 c1) (θ2 A2 c2).
proof: Proof. move=> c1. elim: c1 A2 => [a1|s1 k1 IH1] A2 c2; first by apply commute_ret. simpl; apply commute_bind ; last by move=> a1; apply: IH1. elim: c2 => [a2| s2 k2 IH2] ; first by apply commute_sym, commute_ret. simpl ; apply commute_sym, commute_bind; first by apply commute_sym, Hcom. move=> a2; apply commute_sym, IH2. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads DijkstraMonadExamples) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples)