let resty = C.Appl (outtype::arguments@[term]) in
let resty = NCicReduction.head_beta_reduce ~subst resty in
metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty
let resty = C.Appl (outtype::arguments@[term]) in
let resty = NCicReduction.head_beta_reduce ~subst resty in
metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty