proposition: Theorem prop_subst_term : forall c c' : Prop, forall t, t ⊩ prop c -> (c -> c') -> t ⊩ prop c'.
proof: Proof. subtyping. Qed.
imports: Morphisms ClassicalRealizability.Tactics ClassicalRealizability.BasicResults ClassicalRealizability.Subtyping