proveit.logic.booleans.implication.implies_t_t
proveit.logic.booleans.in_bool_def