NV
dropWithElem : (g : List t) -> Elem a g -> List t
dropWithElem (x::xs) Here = xs
dropWithElem (x::xs) (There el) = dropWithElem xs el
encodeEl : (el : Elem a g) -> Subs g (a::dropWithElem g el)
encodeEl Here = Id
encodeEl (There el) = Comp Shift (encodeEl el)
encode : Term g a -> Tm g a
encode (Var el) = Clos Var (encodeEl el)
encode (Lam t) = Lam $ encode t
encode (App t u) = App (encode t) (encode u)
