Coq's representation of match branches

[aa755]

Our translations assume that Coq represents a match branch for a constructor c a1...an as fun a1 ... an => ..., i.e. the body of the branch begins with as many lambdas as the number of the arguments of the constructor. This is almost always the case. However, for some examples (Gcd Function), Coq seems to violate this invariant. Either template-coq (reifier) or our translation needs to detect such violations and eta-expland to enforce back the invariant.