for n = 1 to arity_consno do
a := (Cic.Implicit None)::(!a)
done;
- (* apply i_inv ? ...? H). *)
- Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
+ (* apply i_inv ? ...? H). *)
+ Cic.Appl ([Cic.Const(uri,[])] @ !a @ [term])
in
let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
let (t1,metasenv,_subst,t3,t4, attrs) = proof in