Exercise 2.
We define a type `tuple` for polymorphic lists with a prescribed length, given
as a parameter. This type is a dependent pair.
This condition is expressed as a (boolean) constraint
on the size of a list, coerced to Prop via the usual `is_true` coercion.
The infix `==` notation refers to the notation available on instances of
the `eqType` structure, as defined by the library loaded in this section.
This structure is isomorphic to the one we used in Lesson 6. In particular, it is endowed with a reflection lemma `eqP`, relating the boolean test with
equality.

Fill the missing parts so that the `test` lemmas are proved without
changing their script.