import proveit
from proveit import x, y
from proveit.logic import Equals, NotEquals, Not, in_bool
from proveit.logic.equality import not_equals_def
from proveit import x, y
theory = proveit.Theory() # the theorem's theory
%proving not_equals_is_bool
not_equals_def
not_equals_def_spec = not_equals_def.instantiate({x:x, y:y})
neg_equals_in_bool = in_bool(Not(Equals(x, y))).prove()
not_equals_def_spec.sub_left_side_into(neg_equals_in_bool)
%qed