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