let qs = proc_bkd_proofs (next st) synth names classes ts in
let lpsno, _ = H.get_ind_type uri tyno in
let ps, _ = H.get_ind_parameters st.context (H.cic v) in
let qs = proc_bkd_proofs (next st) synth names classes ts in
let lpsno, _ = H.get_ind_type uri tyno in
let ps, _ = H.get_ind_parameters st.context (H.cic v) in