[TYPES] HOAS versus meta reasoning - correction

[Andrei Popescu]

Please ignore my remark from the previous posting:

"By the way, approaches around weak HOAS, including Nominal Logic, do not seem to address this issue [that is, representation of inference] at all."

This is of course not true.  What I meant to say is that it appears that 
only strong-HOAS-like settings address the issue of representing inference 
in such a way that typing contexts do not appear explicitly in the 
representation (but are rather embedded shallowly into 
representation-logic contexts).  

Andrei