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