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 =
let rec mkargs = function
| 0 -> []
| 1 -> [Cic.Rel 1]
- | n -> (Cic.Implicit None)::(mkargs (n-1))
+ | n -> (Cic.Rel n)::(mkargs (n-1))
in
mkargs n_lambdas
in