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