fact: Axiom thm_NOT_EX : forall {_35172 : Type'}, forall P : _35172 -> Prop, forall l : list _35172, (~ (@EX _35172 P l)) = (@List.Forall _35172 (fun x : _35172 => ~ (P x)) l).
imports: coq theory_hol types terms axioms