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