triple_of_list : 'a list -> 'a * 'a * 'a
STRUCTURE
SYNOPSIS
Turns a three-element list into a triple.
DESCRIPTION
triple_of_list [x, y, z] returns (x, y, z).
FAILURE
Fails if applied to a list that is not of length 3.
SEEALSO
HOL  Kananaskis-13