mk_pabs : term * term -> term
STRUCTURE
SYNOPSIS
Constructs a paired abstraction.
DESCRIPTION
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.
SEEALSO
HOL  Kananaskis-13