Hello,

There is a question which I don't really quite understand. Can someone explain the answer to me?

I get the first part: the declaration of the "function" however the rest of it I am quite confused. Variables do not need to be declared for this type of exercise.

Insert a sequence at a given location in another sequence.

For example, if the sequence <z,x,z> were to be inserted at location 2 of the sequence <x,y,z>,

the result would be the sequence <x,z,x,z,y,z>.

(Note that this operation is defined only for locations that are within the sequence, in above

example, locations 1, 2 and 3).

The answer is given below.

```
insert: seq X → NAT → seq X ⇸ seq X
n < #t ⇒
(i < n ⇒ (insert s n t) i = t i ∧
n ≤ i < n ⇒ (insert s n t) i = s(i – n + 1) ∧
i ≥ n + #s ⇒ (insert s n t) i = t(i - #s))
```