proposition: Theorem not_all_not_ex_realizer : forall T (A : T -> formula) e, not_all_not_ex↓e ⊩ (¬(∀x, ¬A x)) → ∃x, A x.
proof: Proof. do 2 Ksolve. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping