paraMapFirstAxis : {auto {conArg:12095} : ConsistentWith c cs} -> {auto {conArg:12099} : ConsistentWith c ds} -> Num a => (pf : Tensor cs a -\-> Tensor ds a) -> IsNotDependent pf => Tensor (c :: cs) a -\-> Tensor (c :: ds) aBatching only works simply when we have a non-dependent Para