Si je comprends bien, ce n'est pas encore implanté en typer que la branche du case reçoit une preuve d'égalité entre le sujet du case et la "tête" de la branche?

Yup.

Et additionnellement, si je comprends bien, il semble y avoir un bug qui contourne ce manquement dans certaines preuves comme celle que j'ai faites dans samples/decidable.typer, qui pourrait être relié à ce commentaire: https://gitlab.com/monnier/typer/-/blob/master/btl/builtins.typer#L65-68?

En effet.

Je me demandais ce qu'il manquerait pour implanter cette fonctionnalité.

Pas grand chose: il faut juste l'ajouter dans l'environnement de chaque branche.

D'une part, j'imagine qu'il faudrait ajouter une syntaxe pour avoir accès à cette preuve d'égalité.

Non, c'est pas nécessaire.

La forme (##DeBruijn N) permet déjà de faire référence à n'importe quelle variable, y compris celle qui n'ont pas de nom.

Stefan