proveit.logic.booleans.negation.negation_intro
proveit.logic.booleans.implication.not_iff_via_not_right_impl