dest_prod : hol_type -> hol_type * hol_type
STRUCTURE
LIBRARY
pair
SYNOPSIS
Breaks a product type into its two component types.
DESCRIPTION
dest_prod is a type destructor for products: dest_pair ":t1#t2" returns (":t1",":t2").
FAILURE
Fails with dest_prod if the argument is not a product type.
SEEALSO
HOL  Kananaskis-10