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