proveit.core_expr_types.tuples.range_from1_len_typical_eq
proveit.logic.sets.inclusion.superset_membership_from_proper_subset
proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat