+ | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst ->
+ let _,_,t,_ = List.assoc n subst in
+ let hd = NCicSubstitution.subst_meta lc t in
+ k (*ctx*)
+ (NCicReduction.head_beta_reduce ~upto:(List.length args)
+ (match hd with
+ | NCic.Appl l -> NCic.Appl (l@args)
+ | _ -> NCic.Appl (hd :: args)))