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_via_tuple
%proving sub_in_right_operands_via_tuple
defaults.assumptions = sub_in_right_operands_via_tuple.all_conditions()
operands_substitution_via_tuple
Px_eq_Py = operands_substitution_via_tuple.instantiate({f:P, y:y}, auto_simplify=False)
Px_eq_Py.derive_right_via_equality()
%qed