proposition: Lemma CForall_weak {A} (P Q: A -> Type): (forall x, P x -> Q x) -> (forall l, CForall P l -> CForall Q l).
proof: Proof. induction l; firstorder. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)