+and proc_case st what uri tyno u v ts =
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let synth, classes = I.S.empty, Cl.make ts in
+ let names = H.get_ind_names uri tyno in
+ let qs = proc_bkd_proofs (next st) synth names classes ts in
+ let lpsno, _ = H.get_ind_type uri tyno in
+ let ps, sort_disp = H.get_ind_parameters st.context (H.cic v) in
+ let _, rps = HEL.split_nth lpsno ps in
+ let rpsno = List.length rps in
+ let predicate = clear_absts rpsno (1 - sort_disp) u in
+ let e = Cn.mk_pattern rpsno predicate in
+ let text = "" in
+ let script = List.rev (mk_arg st v) in
+ script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")]
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_preamble st what script
+