Here's the problem, essentially:
tm : type. w : type. hyp : tm -> w -> type. good : type. fact : ({x}{a} hyp x a -> good) -> ({a:w} good). easy : ({x}{a} hyp x a -> good) -> {{a:w} good) -> type. hard : ({x}{a} hyp x a -> {y} hyp y (Q a) -> good) -> ( {a} {y} hyp y (Q a) -> good) -> type.
"easy" should be easy to prove, by using "fact". For "hard", however, I want to hypothesize y : tm and pf : hyp y (Q a) and then appeal to "easy" as a lemma, but I don't have access to a! If I try
hard_proof : hard HYP1 HYP2 <- ({y}{pf:hyp y _} easy ([x][a][h] HYP1 x a h y pf) ([a] HYP2 a y pf)).
then the underscore is reconstructed as merely a first-order Q, without any dependencies, of course, on the a that isn't even in its scope.