[Agda] Dealing with HOAS

[Vag Vagoff]

> What are you trying to do with this representation?
>
>
>   
I'm trying to prove progress and preservation of STLC and System F.

> For the most part this works pretty well and well-scoped deBruijn
> indices are actually not that painful to work with.
De Brujin's encoding is good both for evaluating and reasoning, I know. 
But I'm interested in searching of shallowest embedding first.
> Below I've included code for the first part I described.
Thanks!!!