The context of the higher-order matching problem

The higher-order matching problem is a notoriously difficult decision problem, which was solved by Colin Stirling positively. However, the existing proof is very difficult to understand. I will present the basic definitions concerning the problem and introductory facts necessary for further exposition of Stirling's proof details.