proposition: Theorem not_ex_all_not_realizer : forall T (F : T -> formula), forall e, not_ex_all_not↓e ⊩ ¬(∃x, F x) → ∀x, ¬F x.
proof: Proof. repeat Ksolve. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping