proposition: Lemma neg_equiv : forall e, (λ"t" λ"c" callcc @ λ"k" "t" @ ("k" @ "c"))↓e ⊩ (⊥ → ⊥) → ∀X, X → X.
proof: Proof. do 2 Ksolve. Qed.
imports: ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping