proveit.logic.booleans.conjunction.false_and_false_negated proveit.logic.equality.substitute_falsehood