fact: Fixpoint CNoDup {T: Type} (R: T -> T -> Type) (l: list T): Type := match l with | nil => True | h :: t => prod (CNoDup R t) (CForall (R h) t) end.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)