dest_bool_case : term -> term * term * term
STRUCTURE
SYNOPSIS
Destructs a case expression over bool.
DESCRIPTION
If M has the form bool_case M1 M2 b, then dest_bool_case M returns M1,M2,b.
FAILURE
Fails if M is not a full application of the bool_case constant.
SEEALSO
HOL  Trindemossen-1