The reason I don't want to use coercions here is that I already have coercions and I obtain a diamond situation with several paths with same endpoints. I thought that using type classes was a way to work around this issue.

@AndrejBauer It is not exactly what I had in mind. What I had in mind was: keeping metavariables to write raw rules and using raw rules to present deductive systems (as you do) but the deductive system associated with the raw type theory (the closure rules) would have no metavariables (that is: we would instantiate metavariables with expressions in the original signature). I see why it is nice to have metavariables for raw rules since, as you say, it is how it is actually done but I don't see why we keep them in the closure rules.

@AndrejBauer Thank you! I missed the difference between $\mathcal{b}$ and $\mathcal{B}$. Metavariables are useful for writing raw rules, but would it possible to remove them (and thus remove metavariables contexts and TT-META and TT-META-CONGR rules) from closure rules and thus have closure rules in the original signature?

@AndrejBauer Sorry for bothering you with my questions. Page 57, proof of Lemma 3.6: "By inversion the first premise is derived by an application of TT-Abstr" - does it mean that $Θ;Γ ⊢ {𝑥:𝐴} \mathcal{J}" couldn't be obtained by another rule? I don't see why it could not be obtained by TT-META or by an instantiation of some specific rule.

@AndrejBauer In the comment (3), p. 17 "For example, the correct way to read TT-Abstr is: “For all Θ, Γ, 𝐴, (...)", how should we quantify? "For all type metavariables A" or "For all type expressions A"?

Thanks! For some psychological reason I thought a deductive system couldn't contain hypothetical and boundary judgments together: I see deductive systems as a way to specify derivations and we have either derivations with only hypothetical judgements or with only boundary judgements (right?). If it is right, we could define an associated hypothetical deductive system and an associated boundary deductive system instead of an associated deductive system. If derivations indeed don't mix the two kinds of judgements, it would be equivalent but, perhaps, closer to the intuition.

@AndrejBauer Premises and conclusions of Fig. 2.5 are hypothetical judgements in contrast with those of Fig. 2.6, which are hypothetical boundaries. Thus equality closure rules are really closure rules; more precisely, for instance, the TT-EqTy-Refl rule is not one closure rule but a set of closure rules in the same way as for the TT-Abstr rule as explained in Remark (3): for any metavariable context $\Theta$, for any variable context $\Gamma$, for any metavariable A$, we have one closure rule TT-EqTy-Refl_{\Theta, \Gamma, A}. That's fine to me because I expect to get a set of closure rules.

I didn't understand the question: the Program Fixpoint foo you commented generates an obligation that is trivial because you have the assumption Heq_anonymous : (Some h, t) = hdtl l. Why are you not satisfied with it and are you trying to write another (more complicated) Program Fixpoint foo?