# Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Let $$\ast$$ stand for "type" and $$\square$$ stand for "kind" so that $$\ast:\square$$. Suppose I want to find an inhabitant of $$\Pi x: A.\Pi y:B(x). \ast$$. The derivation rules are given here.

Intuitively, as far as I understand, this inhabitant should have the form $$\lambda x:A.\lambda y:B(x). P(x,y)$$ for some $$P: A\to B(x)\to \ast$$. (If this is not right, let me know.)

Formally, I got to this point. So I proved that $$\lambda y:B(x). P(x,y) : \Pi y:B(x).\ast$$ in a certain context. But then I cannot abstract over $$x:A$$ because the "flag" (assumption) $$P:A\to B(x)\to \ast$$ doesn't let me do so. And I cannot move this flag before the flag "$$x:A$$" because I must assume $$x:A$$ before assuming $$P: A\to B(x) \to \ast$$ since $$B(x)$$ depends on $$x:A$$. What should I do in this situation?

Since you are asking to find any inhabitant, how about $$\lambda (x : A). \lambda y : B(x). A$$?
In other words, we take $$P := \lambda (u : A) . \lambda (v : B u) . A$$. It looks like part of your problem is that you want somehow to use an unspecified $$P$$.