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