proposition: Theorem prop_realizer1' : forall c : Prop, forall t, c -> t ⊩ prop c -> t ⊩ one.
proof: Proof. intros c t Hc Ht. start. apply Ht. left. now split. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping