proposition: Lemma InA_singleton x y : InA eqA x [y] ↔ eqA x y.
proof: Proof. split; intros E. inversion_clear E; auto. now destruct (proj1 (InA_nil eqA x)). rewrite E. intuition. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads