proposition: Lemma top_bot_sub_prop : forall c, (⊤ → ⊥) ⊆ prop c.
proof: Proof. intro c. start. subtyping. split; ok. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping