nodup): change `Type` to `Type u` (#14721)

Commit

3 years ago

fix(data/list/nodup): change `Type` to `Type u` (#14721) Change `Type` to `Type u` in `nodup_iff_nth_ne_nth` and two other lemmas added in #14371.

Author

user7230724

Parents