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