proveit.logic.booleans.unfold_is_bool
proveit.logic.booleans.disjunction.or_if_right