+let rec args_init n f =
+ if n <= 0 then [] else f n :: args_init (pred n) f
+
+let mk_predicate_for_elim
+ ~context ~metasenv ~ugraph ~goal ~arg ~using ~cpattern ~args_no =
+ let instantiated_eliminator =
+ let f n = if n = 1 then arg else C.Implicit None in
+ C.Appl (using :: args_init args_no f)
+ in
+ let _actual_arg, iety, _metasenv', _ugraph =
+ CicRefine.type_of_aux' metasenv context instantiated_eliminator ugraph
+ in
+ let _actual_meta, actual_args = match iety with
+ | C.Meta (i, _) -> i, []
+ | C.Appl (C.Meta (i, _) :: args) -> i, args
+ | _ -> assert false
+ in
+(* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *)
+ let rec mk_pred metasenv context' pred arg' cpattern' = function
+ | [] -> metasenv, pred, arg'
+ | arg :: tail ->
+(* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
+ let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in
+ let argty = CicReduction.whd context argty in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst:[] metasenv context' C.Anonymous ~typ:argty
+ in
+ let hyp = Some (fresh_name, C.Decl argty) in
+ let lazy_term c m u =
+ let distance = List.length c - List.length context in
+ S.lift distance arg, m, u
+ in
+ let pattern = Some lazy_term, [], Some cpattern' in
+ let subst, metasenv, _ugraph, _conjecture, selected_terms =
+ ProofEngineHelpers.select
+ ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern
+ in
+ let metasenv = MS.apply_subst_metasenv subst metasenv in
+ let map (_context_of_t, t) l = t :: l in
+ let what = List.fold_right map selected_terms [] in
+ let arg' = MS.apply_subst subst arg' in
+ let argty = MS.apply_subst subst argty in
+ let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in
+ let pred = MS.apply_subst subst pred in
+ let pred = C.Lambda (fresh_name, argty, pred) in
+ let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in
+ mk_pred metasenv (hyp :: context') pred arg' cpattern' tail
+ in
+ let metasenv, pred, arg =
+ mk_pred metasenv context goal arg cpattern (List.rev actual_args)
+ in
+ HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args));
+ metasenv, pred, arg, actual_args
+