import proveit
from proveit import defaults, Lambda
from proveit import x, y, P, Q, X
from proveit.logic.equality import sub_left_side_into
theory = proveit.Theory() # the theorem's theory
%proving lhs_via_equality
defaults.assumptions = lhs_via_equality.all_conditions()
sub_left_side_into
sub_left_side_into.instantiate({P:Lambda(X, X), x:P, y:Q})
%qed