proveit.logic.booleans.implication.modus_tollens_denial
proveit.logic.booleans.negation.double_negation_intro