metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
| Some arg ->
let gty' = CicSubstitution.subst t1 abstr_gty in
metasenv', C.Meta (fresh_meta,irl), Cic.Rel (-1) (* dummy term, never used *)
| Some arg ->
let gty' = CicSubstitution.subst t1 abstr_gty in