I found two examples in some lecture notes online and I can't follow their approach on the solution. Maybe someone can help.
First they translate from predicate logic to $\lambda$P and then they give an inhabitant of the term. This is what is written in the lecture notes:
An inhabitant of the term $ (\Pi x :\text{Terms}.\text{P x}) \rightarrow (\text{P N}) $ is: $$ \lambda p : (\Pi x : \text{Terms}. \text{P x}) . (\text{p N}) $$
And an inhabitant of the term $ \text{A} \rightarrow (\Pi x : \text{Terms}. \text{A})$ is: $$ \lambda w: \text{A}. \lambda x : \text{Terms}.w $$
However, they didn't explain how they got the inhabitant. It would really help me understand the whole typing theory. Do they derive it via the typing rules? But than I still can't see what rule they would use. Or do you just have to see it?!
Thanks to who ever is helping me in advance!
There's a rule-by-rule correspondence between rules of natural deduction for first-order logic and the typing rules of $\lambda P$.1 Here's a proof of the latter formula (written as $A\to\mathsf{Terms}\to A$ as $\Pi x:A.B$ where $x$ is not free in $B$ is usually taken as the definition of $A\to B$ in dependently typed contexts): $$\dfrac{\dfrac{\dfrac{}{A,\mathsf{Terms}\vdash A}\rlap{\mathsf{Hyp}}}{A\vdash\mathsf{Terms}\to A}\rlap{\to I}}{\vdash A\to\mathsf{Terms}\to A}\rlap{\to I}$$ and here's is the corresponding typing derivation: $$\dfrac{\dfrac{\dfrac{}{x:A,y:\mathsf{Terms}\vdash x: A}\rlap{\mathsf{Hyp}}}{x:A\vdash(\lambda y:\mathsf{Terms}.x):\mathsf{Terms}\to A}\rlap{\to I}}{\vdash (\lambda x:A.\lambda y:\mathsf{Terms}.x) : A\to\mathsf{Terms}\to A}\rlap{\to I}$$
Finding a term of a given type is more or less equivalent to finding a proof of the corresponding formula. It no more (or less) requires needing to "just see it" than finding a proof does. Indeed, if we look for normal form terms then (assuming $A$ and $\mathsf{Terms}$ are primitive types about which we know nothing) this is the only normal form lambda term of this type and it is completely mechanically derivable from the type. In general, though, finding a term, like finding a proof, is hard. Both of these problems2 are semidecidable. If you have a proof though, producing the corresponding lambda term is a straightforward mechanical task.
1 Okay, $\lambda P$ corresponds more to a first-order logic where you can quantify over functions.
2 As indicated, they are really the same problem.