proposition: Lemma CNoDup_weak {A: Type} (Ra Rb: A -> A -> Type) (l: list A): (forall x y, Ra x y -> Rb x y) -> CNoDup Ra l -> CNoDup Rb l.
proof: Proof. Proof with auto. induction l... firstorder. apply CForall_weak with (Ra a)... Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)