proposition: Lemma list_equiv_eq {A} (x y : list A) : @list_equiv A (≡) x y ↔ x ≡ y.
proof: Proof. split. induction 1. reflexivity. now f_equal. intros. now subst. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads