I decided to write transpose with implicit parameters. And get stuck, as usual.
This is partial code: -------------------------------------------------------------------- ( n : Nat ; m : Nat ; xys : Vec n (Vec m X) ! let !---------------------------------------------! ! transpose _n _m xys : Vec m (Vec n X) ) transpose _ n _ m xys <= rec xys { transpose _ n _ m xys <= case xys { transpose _ n _ zero vnil [<= case _n] transpose _ n _ (suc m) (vcons xy xys) [] } } -------------------------------------------------------------------- Why "<= case xys" matches xys and m? The type of xys is clearly says that it depends on n, then on m and matching should be done on xys and n.