[ Contexte: JA est en train de changer la règle du `Case` pour permettre ce qu'on appelle "dependent elimination". Dans notre cas ce qu'on veut faire est d'ajouter dans le contexte de chaque branche une preuve de l'égalité entre le "scrutinee/target" et le motif de la branche. Le problème que JA a alors rencontré est que lors de la normalisation (i.e. `lexp_whnf`), il faut alors fournir cette preuve sous la forme d'un objet `Eq_refl` et que pour ça il faut le type du scrutinee/target (ainsi que son "universe level"); hors ce type n'est pas directement accessible depuis `lexp_whnf`. ]

Salut Jean-Alexandre,

En y réfléchissant un peu plus, voici ce qu'y m'est venu à l'esprit:

- Dans mon article sur CUC, j'évite ce problème en utilisant un `refl` qui est built-in, donc la preuve de `e = e` s'écrit simplement `refl e` plutôt que de devoir écrire `Eq_refl ℓ τₑ e`. On pourrait de même ajouter un `Refl` directement dans `lexp`. Ça me semble pas une solution très élégante, par contre.

- Comme tu l'as mentionné on pourrait calculer `τₑ` à la volée en appelant `get_type`. Par contre c'est pas super pratique et encore moins efficace.

- Une autre approche est d'ajouter `ℓ` et `τₑ` comme annotations sur `Case` pour que ces infos soient directement accessible lors du `lexp_whnf`. C'est pas super-élégant ni super-pratique, mais c'est pas un "hack" et ça ne devrait pas poser de problème de performance. IIRC, certaines présentations papier de CIC utilisent de telles annotations.

- Ces deux arguments sont fondamentalement redondants, on sait pertinemment qu'ils existent, et on va probablement pas les regarder de près, donc un hack serait de simplement y mettre des métavariables.

- On pourrait rendre ce hack plus noble en remplaçant ces métavariables par des "delayed computations".

-- Stefan