Results 2 issues of Olivier Laurent

Add computational content to `List.v`: mainly `Type` is used instead of `Prop` as much as possible. **Kind:** feature. - [ ] Entry added in the changelog

kind: feature
needs: rebase
help wanted
part: standard library
stale

The following link looks broken: https://github.com/math-comp/mcb/blob/c32cc2cada2c123d44b4f345f3812e3b199d478b/tex/chTypeInference.tex#L240 [Page 118](https://zenodo.org/record/3999478): `Chapter ??`.