proveit.logic.booleans.disjunction.false_or_false_negated proveit.logic.equality.substitute_falsehood