 Unsolvable lambda term

An unsolvable lambda term has no head normal form, equivalently it is not a solvable lambda term. Capture-avoiding substitution and lambda application preserve unsolvability: until a head variable appears, head contractions proceed within the original term and cannot inspect the supplied terms.