Hi Dan,
> data Env : Nat -> ...
>
> But, we're stuck there, because the vector depends on the value of the
> natural. I eventually worked out the following encoding:
I think you are allowed to write:
data Env : (n : Nat) -> Vec n -> Set where
...
which avoids having to work with sigma types.
Hope this helps,
Wouter