Add Explicit Reference to Definition of `idahospiders` in 3.5.6 Append Example

In 3.5.6 , `idahospiders` is used in an Append example , but no mention provided on where it was defined had me searching for a while.

An improvement here would be to include a link to 3.4.2 where `idahospiders` was defined with the example.
(here's the link: https://lean-lang.org/functional_programming_in_lean/Overloading-and-Type-Classes/Arrays-and-Indexing/#non-empty-list-indexing)