let ty' = eta_fix [] [] ty in
let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
let ty' = eta_fix [] [] ty in
let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in