The record transformation

After the stipulated tuple isomorphisms, the source has classical arity $m+k$, while the target has type

Both report the same ordered classical pair $(c,x)$. The target also returns the original source register. Left-to-right evaluation completes $u$ before reading the record.

Every retained source name occurs once in the returned tuple. Thus neither term duplicates a quantum name or silently drops a spectator. In particular, $u=\ast$ is legal only when $B=\varnothing$.