proposition: Theorem prop_realizer1 : forall A : Prop, forall e, A -> Id↓e ⊩ prop A.
proof: Proof. intros. start. now apply Id_realizer. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping