proposition: Lemma NoDup_NoDupA {A} (R : relation A) (ls : list A) (R_eq : forall x y, R x y -> x = y) (H : NoDup ls) : NoDupA R ls.
proof: Proof. induction ls; [ solve [ constructor ] | ]. inversion H; subst. constructor; auto. rewrite InA_alt. intros [y [H' H'']]. match goal with | [ H : _ |- _ ] => apply R_eq in H; subst end. tauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts