Proof of proveit.numbers.numerals.decimals.tuple_len_1 theorem

import proveit
from proveit import var_range, ExprTuple
from proveit import a, b, i
from proveit.core_expr_types.tuples  import tuple_len_incr, tuple_len_0
from proveit.logic import InSet
from proveit.numbers import Natural, zero, one
from proveit.numbers.numerals.decimals import md_nine_add_one
theory = proveit.Theory() # the theorem's theory

%proving tuple_len_1

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
tuple_len_1:
(see dependencies)

tuple_len_incr

 ⊢  

tuple_len_0

 ⊢  

tuple_len_0.rhs

# tuple_len_incr.instantiate({i: tuple_len_0.rhs, ExprTuple(var_range(a, one, zero)):tuple_len_0.lhs.operands[0], b:a}, 
#                           assumptions=[InSet(zero, Natural)])

# %qed