let gty'' =
ProofEngineReduction.replace_lifting
~equality:ProofEngineReduction.alpha_equivalence
- ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+ ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
in
- C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+ C.Lambda
+ (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
-prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in
let gty'' =
ProofEngineReduction.replace_lifting
~equality:ProofEngineReduction.alpha_equivalence
- ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+ ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
in
- C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+ C.Lambda
+ (ProofEngineHelpers.mk_fresh_name context C.Anonymous ty, ty, gty'')
in
-prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
let fresh_meta = ProofEngineHelpers.new_meta proof in
let irl =
ProofEngineHelpers.identity_relocation_list_for_metavariable context in