##
Tuple Index

The tuple index operation extracts a specific number from a tuple.
which is an ordered sequence of numbers. For example, if A is a tuple and (= A (<,> (<,> (2) (5)) (7))), then
(= (_ A (1)) (2)), (= (_ A (2)) (5)), and (= (_ A (3)) (7)). The index operation is defined
here. If the index goes above the length
of the tuple, it will still return a number, but this is not a meaningful value and theorems should
be constructed in such a way that the index never goes above the tuple length.

Tuple Overview