metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
| Some arg ->
let gty' = CicSubstitution.subst t1 abstr_gty in
- metasenv,arg,gty'
+ metasenv',arg,gty'
in
let exact_proof =
C.Appl [eq_ind ; ty ; t2 ; pred ; arg ; t1 ;equality]