HOL-ex.Case_Product