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 fold_not_equals
defaults.assumptions = fold_not_equals.conditions
not_equals_def
not_equals_def.instantiate({x:x, y:y}).derive_left_via_equality()
%qed