proveit.logic.booleans.disjunction.true_or_true
proveit.logic.equality.substitute_truth