proveit.logic.booleans.in_bool_def
proveit.logic.booleans.disjunction.binary_closure
proveit.logic.equality.sub_left_side_into