proveit.logic.booleans.disjunction.unary_or_lemma
proveit.logic.booleans.true_is_bool
proveit.logic.booleans.false_eq_false
proveit.logic.equality.sub_left_side_into
proveit.logic.booleans.false_is_bool
proveit.logic.booleans.forall_over_bool_by_cases