proveit.logic.equality.unfold_not_equals
proveit.logic.sets.enumeration.singleton_def
proveit.logic.equality.sub_left_side_into