+ ~subst:[] metasenv context C.Anonymous ~typ:ty in
+ let lifted_t1 = CicSubstitution.lift 1 t1 in
+ let lifted_gty = CicSubstitution.lift 1 gty in
+ let lifted_conjecture =
+ metano,(Some (fresh_name,Cic.Decl ty))::context,lifted_gty in
+ let lifted_pattern = Some lifted_t1,[],CicSubstitution.lift 1 concl_pat in
+ let _,selected_terms_with_context =
+ ProofEngineHelpers.select
+ ~metasenv ~conjecture:lifted_conjecture ~pattern:lifted_pattern in
+ let what,with_what =
+ (* Note: Rel 1 does not live in the context context_of_t *)
+ (* The replace_lifting_csc_0 function will take care of lifting it *)
+ (* to context_of_t *)
+ List.fold_right
+ (fun (context_of_t,t) (l1,l2) -> t::l1, Cic.Rel 1::l2)
+ selected_terms_with_context ([],[]) in
+ let abstr_gty =
+ ProofEngineReduction.replace_lifting_csc 0
+ ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in
+ let gty' = CicSubstitution.subst t2 abstr_gty in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,gty')::metasenv in
+ let pred = C.Lambda (fresh_name, ty, abstr_gty) in