HOL-ex.Simps_Case_Conv_Examples