dest_pair
pairSyntax.dest_pair : term -> term * term
Breaks apart a pair into two separate terms.
dest_pair is a term destructor for pairs: if M is a term of the form
(t1,t2), then dest_pair M returns (t1,t2).
Failure
Fails if M is not a pair.
See also
pairSyntax.mk_pair,
pairSyntax.is_pair,
pairSyntax.strip_pair