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