proveit.logic.equality.fold_not_equals