proveit.core_expr_types.tuples.tuple_len_0_typical_eq
proveit.logic.booleans.conjunction.empty_conjunction_eval