proposition: Lemma callcc_other_realizer : forall A B e, callcc↓e ⊩ ((A → B) → ⊥) → A.
proof: Proof. intros A B e. apply (sub_term (callcc_realizes_Peirce e)). subtyping. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping