proposition: Lemma equivlistA_app_comm l₁ l₂ : equivlistA eqA (l₁ ++ l₂) (l₂ ++ l₁).
proof: Proof. split; apply InA_comm. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads