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.
