1 (* cOpyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
29 (******* CIC substitution ***************************************************)
31 type cic_substitution = Cic.substitution
32 let cic_apply_subst = CicMetaSubst.apply_subst
33 let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
34 let cic_ppsubst = CicMetaSubst.ppsubst
35 let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
36 let cic_flatten_subst subst =
38 (fun (i, (context, term, ty)) ->
39 let context = (* cic_apply_subst_context subst*) context in
40 let term = cic_apply_subst subst term in
41 let ty = cic_apply_subst subst ty in
42 (i, (context, term, ty))) subst
43 let rec cic_lookup_subst meta subst =
45 | Cic.Meta (i, _) -> (
46 try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
47 in cic_lookup_subst t subst
48 with Not_found -> meta
53 let cic_merge_subst_if_possible s1 s2 =
54 let already_in = Hashtbl.create 13 in
55 let rec aux acc = function
56 | ((i,_,x) as s)::tl ->
58 let x' = Hashtbl.find already_in i in
59 if x = x' then aux acc tl else None
62 Hashtbl.add already_in i x;
69 (******** NAIF substitution **************************************************)
71 * naif version of apply subst; the local context of metas is ignored;
72 * we assume the substituted term must be lifted according to the nesting
74 * Alternatively, we could used implicit instead of metas
77 type naif_substitution = (int * Cic.term) list
79 let naif_apply_subst subst term =
83 | Cic.Var (uri,exp_named_subst) ->
84 let exp_named_subst' =
85 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
87 Cic.Var (uri, exp_named_subst')
90 aux k (CicSubstitution.lift k (List.assoc i subst))
94 | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
95 | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
96 | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
97 | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
98 | Cic.Appl [] -> assert false
99 | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
100 | Cic.Const (uri,exp_named_subst) ->
101 let exp_named_subst' =
102 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
104 if exp_named_subst' != exp_named_subst then
105 Cic.Const (uri, exp_named_subst')
107 t (* TODO: provare a mantenere il piu' possibile sharing *)
108 | Cic.MutInd (uri,typeno,exp_named_subst) ->
109 let exp_named_subst' =
110 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
112 Cic.MutInd (uri,typeno,exp_named_subst')
113 | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
114 let exp_named_subst' =
115 List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
117 Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
118 | Cic.MutCase (sp,i,outty,t,pl) ->
119 let pl' = List.map (aux k) pl in
120 Cic.MutCase (sp, i, aux k outty, aux k t, pl')
122 let len = List.length fl in
125 (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
128 | Cic.CoFix (i, fl) ->
129 let len = List.length fl in
131 List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
138 (* naif version of apply_subst_metasenv: we do not apply the
139 substitution to the context *)
141 let naif_apply_subst_metasenv subst metasenv =
143 (fun (n, context, ty) ->
144 (n, context, naif_apply_subst subst ty))
146 (fun (i, _, _) -> not (List.mem_assoc i subst))
149 let naif_ppsubst names subst =
150 "{" ^ String.concat "; "
153 Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
157 let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
159 let naif_flatten_subst subst =
160 List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
163 let rec naif_lookup_subst meta subst =
167 naif_lookup_subst (List.assoc i subst) subst
173 let naif_merge_subst_if_possible s1 s2 =
174 let already_in = Hashtbl.create 13 in
175 let rec aux acc = function
176 | ((i,x) as s)::tl ->
178 let x' = Hashtbl.find already_in i in
179 if x = x' then aux acc tl else None
182 Hashtbl.add already_in i x;
189 (********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
191 type substitution = naif_substitution
192 let apply_subst = naif_apply_subst
193 let apply_subst_metasenv = naif_apply_subst_metasenv
194 let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
195 let buildsubst = naif_buildsubst
196 let flatten_subst = naif_flatten_subst
197 let lookup_subst = naif_lookup_subst
199 (* filter out from metasenv the variables in substs *)
200 let filter subst metasenv =
203 try let _ = List.find (fun (i, _) -> m = i) subst in false
204 with Not_found -> true)
208 let is_in_subst i subst = List.mem_assoc i subst;;
210 let merge_subst_if_possible = naif_merge_subst_if_possible;;
212 let empty_subst = [];;
214 (********* EQUALITY **********************************************************)
216 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
217 type uncomparable = int -> int
219 uncomparable * (* trick to break structural equality *)
222 (Cic.term * (* type *)
223 Cic.term * (* left side *)
224 Cic.term * (* right side *)
225 Utils.comparison) * (* ordering *)
226 Cic.metasenv * (* environment for metas *)
228 and proof = new_proof * old_proof
232 | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)
234 | NoProof (* term is the goal missing a proof *)
235 | BasicProof of substitution * Cic.term
237 substitution * UriManager.uri *
238 (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
239 | ProofGoalBlock of old_proof * old_proof
240 | ProofSymBlock of Cic.term list * old_proof
241 | SubProof of Cic.term * int * old_proof
242 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
247 let id_to_eq = Hashtbl.create 1024;;
255 Hashtbl.clear id_to_eq
258 let uncomparable = fun _ -> 0
260 let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
261 let id = freshid () in
262 let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
263 Hashtbl.add id_to_eq id eq;
267 let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
268 (weight,proof,(ty,l,r,o),m,id)
270 let string_of_equality ?env eq =
273 let w, _, (ty, left, right, o), _ , id = open_equality eq in
274 Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
275 id w (CicPp.ppterm ty)
277 (Utils.string_of_comparison o) (CicPp.ppterm right)
278 | Some (_, context, _) ->
279 let names = Utils.names_of_context context in
280 let w, _, (ty, left, right, o), _ , id = open_equality eq in
281 Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
282 id w (CicPp.pp ty names)
283 (CicPp.pp left names) (Utils.string_of_comparison o)
284 (CicPp.pp right names)
287 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
288 Pervasives.compare s1 s2
291 let rec string_of_proof_old ?(names=[]) = function
292 | NoProof -> "NoProof "
293 | BasicProof (s, t) -> "BasicProof(" ^
294 ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
295 | SubProof (t, i, p) ->
296 Printf.sprintf "SubProof(%s, %s, %s)"
297 (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
298 | ProofSymBlock (_,p) ->
299 Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
300 | ProofBlock (subst, _, _, _ ,(_,eq),old) ->
301 let _,(_,p),_,_,_ = open_equality eq in
302 "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
303 string_of_proof_old p ^ ")"
304 | ProofGoalBlock (p1, p2) ->
305 Printf.sprintf "ProofGoalBlock(%s, %s)"
306 (string_of_proof_old p1) (string_of_proof_old p2)
312 let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
315 Not_found -> assert false
318 let string_of_proof_new ?(names=[]) p gp =
319 let str_of_rule = function
320 | SuperpositionRight -> "SupR"
321 | SuperpositionLeft -> "SupL"
322 | Demodulation -> "Demod"
324 let str_of_pos = function
325 | Utils.Left -> "left"
326 | Utils.Right -> "right"
328 let fst4 (x,_,_,_) = x in
329 let rec aux margin name =
330 let prefix = String.make margin ' ' ^ name ^ ": " in function
332 Printf.sprintf "%sExact (%s)\n"
333 prefix (CicPp.pp t names)
334 | Step (subst,(rule,eq1,(pos,eq2),pred)) ->
335 Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
336 prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
337 (CicPp.pp pred names)^
338 aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^
339 aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2))
346 "GOAL: %s %d %s %s\n"
347 (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^
348 aux 1 (Printf.sprintf "%d " i) (fst4 (proof_of_id i)))
352 let ppsubst = ppsubst ~names:[]
354 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
355 let build_ens_for_sym_eq sym_eq_URI termlist =
356 let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
358 | Cic.Constant (_, _, _, uris, _) ->
359 assert (List.length uris <= List.length termlist);
360 let rec aux = function
362 | (uri::uris), (term::tl) ->
363 let ens, args = aux (uris, tl) in
364 (uri, term)::ens, args
365 | _, _ -> assert false
371 let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
372 let rec do_build_proof proof =
375 Printf.fprintf stderr "WARNING: no proof!\n";
377 | BasicProof (s,term) -> apply_subst s term
378 | ProofGoalBlock (proofbit, proof) ->
379 print_endline "found ProofGoalBlock, going up...";
380 do_build_goal_proof proofbit proof
381 | ProofSymBlock (termlist, proof) ->
382 let proof = do_build_proof proof in
383 let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
384 Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
385 | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
386 let t' = Cic.Lambda (name, ty, bo) in
387 let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
388 let proof' = do_build_proof proof in
389 let eqproof = do_build_proof eqproof in
391 if pos = Utils.Left then what, other else other, what
394 (Cic.Appl [Cic.Const (eq_URI, []); ty;
395 what; t'; eqproof; other; proof'])
396 | SubProof (term, meta_index, proof) ->
397 let proof = do_build_proof proof in
399 | Cic.Meta (j, _) -> i = j
402 ProofEngineReduction.replace
403 ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
405 and do_build_goal_proof proofbit proof =
407 | ProofGoalBlock (pb, p) ->
408 do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
409 | _ -> do_build_proof (replace_proof proofbit proof)
411 and replace_proof newproof = function
412 | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
413 let eqproof' = replace_proof newproof eqproof in
414 ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
415 | ProofGoalBlock (pb, p) ->
416 let pb' = replace_proof newproof pb in
417 ProofGoalBlock (pb', p)
418 | BasicProof _ -> newproof
419 | SubProof (term, meta_index, p) ->
420 SubProof (term, meta_index, replace_proof newproof p)
426 let build_proof_term_new proof =
427 let rec aux extra = function
428 | Exact term -> term, []
429 | Step (subst,(_, id1, (pos,id2), pred)) ->
430 let p,m1,_,_ = proof_of_id id1 in
431 let p1,m2 = aux [] p in
432 let p,m3,l,r = proof_of_id id2 in
433 let p2,m4 = aux [] p in
434 let p1 = apply_subst subst p1 in
435 let p2 = apply_subst subst p2 in
436 let l = apply_subst subst l in
437 let r = apply_subst subst r in
438 let pred = apply_subst subst pred in
439 let ty = (* Cic.Implicit None *)
441 | Cic.Lambda (_,ty,_) -> ty
444 let what, other = (* Cic.Implicit None, Cic.Implicit None *)
445 if pos = Utils.Left then l,r else r,l
449 | Utils.Left -> Utils.eq_ind_URI ()
450 | Utils.Right -> Utils.eq_ind_r_URI ()
453 Cic.Const (eq_URI, []);
454 ty; what; pred; p1; other; p2]),
455 (apply_subst_metasenv subst (m1@m2@m3@m4))
460 let build_goal_proof l (refl,reflmenv) =
461 let proof, menv, subst =
463 (fun (current_proof,current_menv,current_subst) (pos,id,subst,pred) ->
464 let p,m,l,r = proof_of_id id in
465 let p,m1 = build_proof_term_new p in
466 let p = apply_subst subst p in
467 let l = apply_subst subst l in
468 let r = apply_subst subst r in
469 let pred = apply_subst subst pred in
470 let newm = apply_subst_metasenv subst (m@m1) in
471 let ty = (* Cic.Implicit None *)
473 | Cic.Lambda (_,ty,_) -> ty
476 let what, other = (* Cic.Implicit None, Cic.Implicit None *)
477 if pos = Utils.Right then l,r else r,l
481 | Utils.Left -> Utils.eq_ind_r_URI ()
482 | Utils.Right -> Utils.eq_ind_URI ()
484 ((Cic.Appl [Cic.Const (eq_URI, []);
485 ty; what; pred; current_proof; other; p]),
486 current_menv @ newm, subst @ current_subst))
492 let refl_proof ty term =
495 (LibraryObjects.eq_URI (), 0, 1, []);
499 let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
501 let relocate newmeta menv =
502 let subst, metasenv, newmeta =
504 (fun (i, context, ty) (subst, menv, maxmeta) ->
506 CicMkImplicit.identity_relocation_list_for_metavariable context *)
508 let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
509 let newmeta = maxmeta, context, ty in
510 newsubst, newmeta::menv, maxmeta+1)
511 menv ([], [], newmeta+1)
513 let metasenv = apply_subst_metasenv subst metasenv in
514 let subst = flatten_subst subst in
515 subst, metasenv, newmeta
518 let fix_metas newmeta eq =
519 let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
522 fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
523 prerr_endline (string_of_equality eq); *)
524 let subst, metasenv, newmeta = relocate newmeta menv in
525 let ty = apply_subst subst ty in
526 let left = apply_subst subst left in
527 let right = apply_subst subst right in
528 let fix_proof = function
530 | BasicProof (subst',term) -> BasicProof (subst@subst',term)
531 | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
535 (fun (i, (context, term, ty)) ->
536 let context = apply_subst_context subst context in
537 let term = apply_subst subst term in
538 let ty = apply_subst subst ty in
539 (i, (context, term, ty))) subst' in *)
540 ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
543 let fix_new_proof = function
544 | Exact p -> Exact (apply_subst subst p)
545 | Step (s,(r,id1,(pos,id2),pred)) ->
546 Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
548 let new_p = fix_new_proof p1 in
549 let old_p = fix_proof p2 in
550 let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
551 (* debug prerr_endline (string_of_equality eq); *)
554 exception NotMetaConvertible;;
556 let meta_convertibility_aux table t1 t2 =
557 let module C = Cic in
558 let rec aux ((table_l, table_r) as table) t1 t2 =
560 | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
561 let m1_binding, table_l =
562 try List.assoc m1 table_l, table_l
563 with Not_found -> m2, (m1, m2)::table_l
564 and m2_binding, table_r =
565 try List.assoc m2 table_r, table_r
566 with Not_found -> m1, (m2, m1)::table_r
568 if (m1_binding <> m2) || (m2_binding <> m1) then
569 raise NotMetaConvertible
575 | None, Some _ | Some _, None -> raise NotMetaConvertible
577 | Some t1, Some t2 -> (aux res t1 t2))
578 (table_l, table_r) tl1 tl2
579 with Invalid_argument _ ->
580 raise NotMetaConvertible
582 | C.Var (u1, ens1), C.Var (u2, ens2)
583 | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
584 aux_ens table ens1 ens2
585 | C.Cast (s1, t1), C.Cast (s2, t2)
586 | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
587 | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
588 | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
589 let table = aux table s1 s2 in
591 | C.Appl l1, C.Appl l2 -> (
592 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
593 with Invalid_argument _ -> raise NotMetaConvertible
595 | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
596 when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
597 | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
598 when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
599 aux_ens table ens1 ens2
600 | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
601 when (UriManager.eq u1 u2) && i1 = i2 ->
602 let table = aux table s1 s2 in
603 let table = aux table t1 t2 in (
604 try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
605 with Invalid_argument _ -> raise NotMetaConvertible
607 | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
610 (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
611 if i1 <> i2 then raise NotMetaConvertible
613 let res = (aux res s1 s2) in aux res t1 t2)
615 with Invalid_argument _ -> raise NotMetaConvertible
617 | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
620 (fun res (n1, s1, t1) (n2, s2, t2) ->
621 let res = aux res s1 s2 in aux res t1 t2)
623 with Invalid_argument _ -> raise NotMetaConvertible
625 | t1, t2 when t1 = t2 -> table
626 | _, _ -> raise NotMetaConvertible
628 and aux_ens table ens1 ens2 =
629 let cmp (u1, t1) (u2, t2) =
630 Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
632 let ens1 = List.sort cmp ens1
633 and ens2 = List.sort cmp ens2 in
636 (fun res (u1, t1) (u2, t2) ->
637 if not (UriManager.eq u1 u2) then raise NotMetaConvertible
640 with Invalid_argument _ -> raise NotMetaConvertible
646 let meta_convertibility_eq eq1 eq2 =
647 let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
648 let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
651 else if (left = left') && (right = right') then
653 else if (left = right') && (right = left') then
657 let table = meta_convertibility_aux ([], []) left left' in
658 let _ = meta_convertibility_aux table right right' in
660 with NotMetaConvertible ->
662 let table = meta_convertibility_aux ([], []) left right' in
663 let _ = meta_convertibility_aux table right left' in
665 with NotMetaConvertible ->
670 let meta_convertibility t1 t2 =
675 ignore(meta_convertibility_aux ([], []) t1 t2);
677 with NotMetaConvertible ->
681 exception TermIsNotAnEquality;;
683 let term_is_equality term =
684 let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
686 | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
690 let equality_of_term proof term =
691 let eq_uri = LibraryObjects.eq_URI () in
692 let iseq uri = UriManager.eq uri eq_uri in
694 | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
695 let o = !Utils.compare_terms t1 t2 in
696 let stat = (ty,t1,t2,o) in
697 let w = Utils.compute_equality_weight stat in
698 let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
701 raise TermIsNotAnEquality
704 let is_weak_identity eq =
705 let _,_,(_,left, right,_),_,_ = open_equality eq in
706 left = right || meta_convertibility left right
709 let is_identity (_, context, ugraph) eq =
710 let _,_,(ty,left,right,_),menv,_ = open_equality eq in
712 (* (meta_convertibility left right)) *)
713 fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
717 let term_of_equality equality =
718 let _, _, (ty, left, right, _), menv, _= open_equality equality in
719 let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
720 let argsno = List.length menv in
722 CicSubstitution.lift argsno
723 (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
727 (fun (i,_,ty) (n, t) ->
728 let name = Cic.Name ("X" ^ (string_of_int n)) in
729 let ty = CicSubstitution.lift (n-1) ty in
731 ProofEngineReduction.replace
732 ~equality:eq ~what:[i]
733 ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
735 (n-1, Cic.Prod (name, ty, t)))