proveit.logic.booleans.in_bool_if_true
proveit.logic.booleans.disjunction.demorgans_law_and_to_or_bin_explicit