Olivier Laurent

This comes from the development of the [yalla](https://perso.ens-lyon.fr/olivier.laurent/yalla/) library (a library for the formalization of linear logic results in Coq). I'll give other justifications but let me explain the path...

@herbelin > Somehow, I would however lean to add the `Type` version already in `List` rather than creating a new file. The reason is that I'm worrying that the files...

@herbelin > Do you know why the `C` variants in `Classes` are not enough? Is it to keep some control on the generation of universe variables? Is it to have...

I am stuck with the two CI failures: - The metacoq one is due to some extraction "not handled yet". Is there a standard solution? I do not see it...

@coqbot ci minimize

The ci-rewriter failure corresponds to the following minimized problem: ```coq Definition atTrue : (Type -> Type) -> Type := fun f => f True. Check (0, atTrue). Definition prod_atTrue :...

Not sure: there does not seem to be rewriting involved. Could it be related with `template`/`universe` polymorphism? ```coq Definition atTrue : (Type -> Type) -> Type := fun f =>...

What should be done then: - declare some objects universe polymorphic? - remove test on `fold_right` in mit-plv/rewriter? - remove `Forall_inf_fold_right` and `fold_right_Forall_inf` from the current PR? I see there...

OK I'll try, thanks. `_inf` is for `_informative` [apparently](https://github.com/coq/coq/pull/11966#issuecomment-618061619) (I used `_Type` previously).

> ``` > Lemma NoDup_decidable_eq {A:Type}: > (decidable_eq A /\ exists (l:list A), Full l) > (exists (l:list A), Full l /\ NoDup l). > ``` This seems to be...