import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit import f, P, x, y
from proveit.core_expr_types.operations import operands_substitution
%proving sub_in_left_operands
defaults.assumptions = sub_in_left_operands.all_conditions()
operands_substitution
Px_eq_Py = operands_substitution.instantiate({f:P, y:y}, auto_simplify=False)
Px_eq_Py.derive_left_via_equality()
%qed