proposition: Lemma prop_sub_one : forall c, prop c ⊆ one.
proof: Proof. intro c. start. elim (Classical_Prop.classic c); intro Hc. now left; split. right. split; subtyping. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping