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