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