proveit.logic.equality.substitute_truth