proposition: Lemma not_impl4_realizer : forall e, not_impl4↓e ⊩ ∀A B C D E, ¬(A → B → C → D → E) → (A ∧ B ∧ C ∧ D ∧ ¬E).
proof: Proof. Ksolve. startn 1. now eapply callcc_other_realizer; find. startn 1. eapply (callcc_other_realizer _ (C → D → E)); find. do 2 Ksolve. startn 1. eapply (callcc_other_realizer _ (D → E)); find. do 2 Ksolve. startn 1. eapply callcc_other_realizer; find. do 2 Ksolve. eok. do 2 Ksolve. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping