proveit.logic.booleans.disjunction.not_right_if_neither