+ let replaced = ref false in
+ let replace = ProofEngineReduction.replace_lifting
+ ~equality:(fun _ a b -> let rc = CicUtil.alpha_equivalence a b in
+ if rc then replaced := true; rc)
+ ~context:[]
+ in
+ let captured =
+ replace ~what:[CicSubstitution.lift n_lambdas term]
+ ~with_what:[Cic.Rel 1] ~where:lifted_ty
+ in
+ if not !replaced then
+ (* this means the matched term is not there,
+ * but maybe right params are: we user rels (to right args lambdas) *)
+ replace ~what ~with_what:(with_what false) ~where:captured
+ else
+ (* since the matched is there, rights should be inferrable *)
+ replace ~what ~with_what:(with_what true) ~where:captured