mk_pabs
pairSyntax.mk_pabs : term * term -> term
Constructs a paired abstraction.
If M is the tuple (v1,..(..)..,vn), and N is an arbitrary term,
then mk_pabs (M,N) returns the paired abstraction
`\(v1,..(..)..,vn).N`.
Failure
Fails unless M is an arbitrarily nested pair composed from variables,
with no repetitions of variables.