proposition: Lemma NoDupA_altdef : forall l, NoDupA l <-> ForallOrdPairs (complement eqA) l.
proof: Proof. split; induction 1 as [|a l H rest]; constructor; auto. - rewrite Forall_forall. intros b Hb. intro Eq; elim H. rewrite InA_alt. exists b; auto. - rewrite InA_alt; intros (a' & Haa' & Ha'). rewrite Forall_forall in H. exact (H a' Ha' Haa'). Qed.
imports: List Sorted Setoid Basics Morphisms