let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in
let pred = C.Lambda (fresh_name, ty, abstr_gty) in
(* The argument is either a meta if we are rewriting in the conclusion
let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in
let pred = C.Lambda (fresh_name, ty, abstr_gty) in
(* The argument is either a meta if we are rewriting in the conclusion