[Epigram] Transpose again

[Serguey Zefirov]

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.