proposition: Lemma CNoDup_map {A B: Type} (R: B -> B -> Type) (f: A -> B): forall l, CNoDup (fun x y => R (f x) (f y)) l IFF CNoDup R (map f l).
proof: Proof. Proof with auto; intuition. induction l; simpl... split; intro; split. apply IHl, X. apply CForall_map... apply IHl, X. apply CForall_map... Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)