import proveit
from proveit import defaults
from proveit import x, Px
theory = proveit.Theory() # the theorem's theory
%proving substitute_in_true
defaults.assumptions = substitute_in_true.all_conditions()
x_eq_T = x.evaluation()
x_eq_T.sub_right_side_into(Px)
%qed