proveit.core_expr_types.tuples.tuple_len_0_typical_eq
proveit.logic.booleans.disjunction.empty_disjunction_eval