proveit.logic.booleans.implication.modus_tollens_affirmation
proveit.logic.booleans.negation.double_negation_intro