proposition: Theorem prop_realizer2' : forall c t, ~c -> t ⊩ prop c -> t ⊩ ⊤ → ⊥.
proof: Proof. intros c t Hc Ht. start. apply Ht. right. repeat split; ok. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping