axiom not_ex_all_demorgan_i: !p:set prop.~ (?x:set.p x) -> !x:set.~ p x axiom dneg: !P:prop.~ ~ P -> P claim !p:set prop.~ (!x:set.p x) -> ?x:set.~ p x