proposition: Lemma top_bot_sub_one : (⊤ → ⊥) ⊆ one.
proof: Proof. unfold one. Ksolve. Qed.
imports: RelationClasses Morphisms ClassicalRealizability.ShallowEmbedding ClassicalRealizability.Tactics ClassicalRealizability.BasicResults