- let g st v ts = g st (C.MutCase (uri, tyno, outty, v, ts)) in
- g st arg cases
+ let g st v =
+ let g (st, ts) = g st (C.MutCase (uri, tyno, outty, v, ts)) in
+ let map h v (st, vs) =
+ let h st vv = h (st, vv :: vs) in opt_proof h st es c v
+ in
+ if es then H.list_fold_right_cps g map cases (st, []) else g (st, cases)
+ in
+ if es then opt_proof g st es c arg else g st arg