underPis : Int -> Env Term vars -> Term vars -> (bnds : SnocList Name ** (Env Term (bnds <>> vars), Term (bnds <>> vars)))
Go under n Pis (if n < 0 then go under as many as possible)