let abstr_gty =
ProofEngineReduction.replace_lifting_csc 0
~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in
+ if lifted_gty = abstr_gty then
+ raise (ProofEngineTypes.Fail (lazy "nothing to do"));
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