Demonstrates how to model nested-arrays, i.e., arrays of arrays in SBV. Instead of SMTLib's nested model, in SBV we use a tuple as an index, which is isomorphic to nested arrays.