- | (k, e, ens, (C.Meta _ as t), s) ->
- let t' = unwind k e ens t in
- if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+ | (k, e, ens, (C.Meta (n,l) as t), s) ->
+ (try
+ let (_, term,_) = CicUtil.lookup_subst n subst in
+ reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
+ with CicUtil.Subst_not_found _ ->
+ let t' = unwind k e ens t in
+ if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))