proposition: Lemma equivlistA_cons_nil x l : ¬equivlistA eqA (x :: l) [].
proof: Proof. intros E. now eapply InA_nil, E, InA_cons_hd. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads