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