proveit.logic.booleans.negation.double_negation_elim