proposition: Lemma CdeMorgan_ex_all : forall (A : Type) (P : A -> CProp) (X : Type), (sigT P -> X) -> forall a : A, P a -> X.
proof: Proof. intros A P X H a H0. eauto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)