import proveit
from proveit import a, b, e, i
from proveit.core_expr_types.tuples import tuple_len_incr
from proveit.numbers.numerals.decimals import tuple_len_4, add_4_1
theory = proveit.Theory() # the theorem's theory
%proving tuple_len_5
four_spec = tuple_len_4.instantiate({a:a}, auto_simplify=False)
tuple_spec = tuple_len_incr.instantiate(
{i: four_spec.rhs, a: four_spec.lhs.operands, b: e})
%qed