proposition: Theorem prop_subst_stack : forall c c' : Prop, forall s, s ∈ ‖prop c'‖ -> (c -> c') -> s ∈ ‖prop c‖.
proof: Proof. intros c c' s Hs Hcc'. elim (Classical_Prop.classic c); intro Hc. left. split. ok. dec s. ok. absurd c'; tauto. right. split. ok. apply (top_bot_sub_prop Hs). Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping