proposition: Lemma CNoDup_indexed {T} (R: T -> T -> Type) (Rsym: Csymmetric _ R) (l: list T) (d: T): CNoDup R l -> forall i j, (i < length l)%nat -> (j < length l)%nat -> i <> j -> R (nth i l d) (nth j l d).
proof: Proof. Proof with intuition. induction l; simpl... exfalso... destruct i. destruct j... apply (CForall_indexed (R a) l)... destruct j... apply Rsym. apply (CForall_indexed (R a) l)... Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)