| NCic.Meta (n,lc) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
k ctx (NCicSubstitution.subst_meta lc t)
| NCic.Meta (n,(s,l)) ->
(* CSC: qua non dovremmo espandere *)
let l = NCicUtils.expand_local_context l in
| NCic.Meta (n,lc) when List.mem_assoc n subst ->
let _,_,t,_ = List.assoc n subst in
k ctx (NCicSubstitution.subst_meta lc t)
| NCic.Meta (n,(s,l)) ->
(* CSC: qua non dovremmo espandere *)
let l = NCicUtils.expand_local_context l in