let status, ty = typeof status (ctx_of what) what in
let status, (ref, consno, _, _) = analyse_indty status ty in
let status, what = term_of_cic_term status what (ctx_of gty) in
let status, ty = typeof status (ctx_of what) what in
let status, (ref, consno, _, _) = analyse_indty status ty in
let status, what = term_of_cic_term status what (ctx_of gty) in