Now, the axioms are essentially these, and what this essentially says is that there in an infinite number of free variables. This says that you can always find a higher order object which when instantiated on a variable which does not occur in it produces the term in question. So every time you have a term with a variable you can always find a higher order object which corresponds to the abstraction of that term. And then the other one is some kind of extensionally quality of contexts.

---