proposition: Corollary not_all_ex_not_realizer4 : forall T S R Q (F : T -> S -> R -> Q -> formula), forall e, not_all_ex_not↓e ⊩ ¬(∀x y z t, F x y z t) → ∃x y z t, ¬F x y z t.
proof: Proof. do 3 Ksolve. eok. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping