| NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
| NCic.Meta (i,_) ->
(try
let _,_,t,_ = List.assoc i subst in
with Not_found -> true)
| NCic.Appl (NCic.Meta (i,_) :: args)->
(try
let _,_,t,_ = List.assoc i subst in
with Not_found -> true)
| NCic.Appl (NCic.Meta (i,_) :: args)->
(try
let _,_,t,_ = List.assoc i subst in
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->
match l with
| _, NCic.Irl _ -> fun _ _ _ _ _ -> None
| shift, NCic.Ctx l -> fun metasenv subst context k t ->