proposition: Lemma equivlistA_permute_heads x y l : equivlistA eqA (x :: y :: l) (y :: x :: l).
proof: Proof. split; apply InA_permute_heads. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads