proposition: Lemma NoDupA_singleton x : NoDupA eqA [x].
proof: Proof. apply NoDupA_cons. intros E. inversion E. auto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads