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