let status, what = disambiguate status what None (ctx_of goalty) in
let status, ty_what = typeof status (ctx_of what) what in
let status, (r,consno,lefts,rights) = analyse_indty status ty_what in
let status, what = disambiguate status what None (ctx_of goalty) in
let status, ty_what = typeof status (ctx_of what) what in
let status, (r,consno,lefts,rights) = analyse_indty status ty_what in