let goalty = get_goalty status goal in
let status,sort = typeof status (ctx_of goalty) goalty in
let status, sort = fix_sorts status sort in
let goalty = get_goalty status goal in
let status,sort = typeof status (ctx_of goalty) goalty in
let status, sort = fix_sorts status sort in