let n_lambdas = n_right_args + 1 in
let lifted_ty = CicSubstitution.lift n_lambdas ty in
let replace = ProofEngineReduction.replace_lifting
- ~equality:(ProofEngineReduction.alpha_equivalence)
+ ~equality:(CicUtil.alpha_equivalence)
in
let captured_ty =
let what =