withArgs package:Agda
xs `withArgsFrom` args translates
xs into a list of
Args, using the elements in
args to fill in the
non-
unArg fields.
Precondition: The two lists should have equal length.
Count the number of arguments introduced into the type of the
with-function.