proposition: Lemma distr_subtype : forall A B : Prop, prop (A -> B) ⊆ (prop A → prop B).
proof: Proof. intros A B. start. left. split. easy. elim (Classical_Prop.classic A); intro HA. exists one. split. start. apply Ht. left. now split. ok. exists (⊤ → ⊥). unfold one in *. Ksolve. start. apply Ht. right. repeat split; ok. elim (Classical_Prop.classic A); intro HA. right. split. tauto. split; ok. left. split. tauto. exists (⊤ → ⊥). Ksolve. Ksolve. right. repeat split; ok. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping