in
let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
let (t1,metasenv,_subst,t3,t4, attrs) = proof in
let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
in
let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
let (t1,metasenv,_subst,t3,t4, attrs) = proof in
let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t