(CicSubstitution.lift 1 termty)
isSetType (CicSubstitution.lift 1 term))
| [] -> ProofEngineReduction.replace_lifting
- ~equality:(ProofEngineReduction.alpha_equivalence)
+ ~equality:(fun _ -> CicUtil.alpha_equivalence)
+ ~context:[]
~what: (if isSetType
then (rightparameters_ @ [term] )
else (rightparameters_ ) )
| [] when isSetType -> Cic.Lambda (
(Cic.Name ("lambda" ^ (string_of_int nright))),
(ProofEngineReduction.replace_lifting
- ~equality:(ProofEngineReduction.alpha_equivalence)
+ ~equality:(fun _ -> CicUtil.alpha_equivalence)
+ ~context:[]
~what: (rightparameters_ )
~with_what: (List.map (CicSubstitution.lift (-1)) created_vars)
~where:termty), (* type of H with replaced right parameters *)