let n_lambdas = n_right_args + 1 in
let lifted_ty = CicSubstitution.lift n_lambdas ty in
let replace = ProofEngineReduction.replace_lifting
let n_lambdas = n_right_args + 1 in
let lifted_ty = CicSubstitution.lift n_lambdas ty in
let replace = ProofEngineReduction.replace_lifting