proveit.logic.booleans.negation.negation_contradiction
proveit.logic.booleans.negation.negation_intro