import proveit
from proveit import defaults
from proveit import f, x, y, P, Px, Py
from proveit.logic import Equals
from proveit.logic.equality import substitution
theory = proveit.Theory() # the theorem's theory
%proving sub_left_side_into
defaults.assumptions = sub_left_side_into.all_conditions()
substitution
# P(x)=P(y) from x=y via substitution
substitution.instantiate({f:P, x:x, y:y})
Py.prove().evaluation()
# P(x)=TRUE via P(y)=TRUE and transitivity
Px.evaluation()
%qed