proposition: Theorem prop_realizer2 : forall A : Prop, forall e, ~A -> nId↓e ⊩ ¬(prop A).
proof: Proof. intros A e HA. start. apply Ht. right. repeat split; ok. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping