proposition: Lemma equivlistA_app_nil_l l : equivlistA eqA ([] ++ l) l.
proof: Proof. reflexivity. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads