proposition: Theorem not_all_ex_not_realizer : forall T (F : T -> formula), forall e, not_all_ex_not↓e ⊩ ¬(∀x, F x) → ∃x, ¬F x.
proof: Proof. do 3 Ksolve. eok. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping