X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.ml;h=3bff5b57460bc4decc952b913a83f4c410fb4d29;hb=08a92d276c5477968b02f31097b6ed03185f34eb;hp=953635dbd8e65df346c11dbc45c0f683f4c3d42f;hpb=ac9ab5d3ada1d5ea4a4ac00aee7e6bc456f4e98c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 953635dbd..3bff5b574 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -25,194 +25,6 @@
 
 (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
 
-
-(******* CIC substitution ***************************************************)
-
-type cic_substitution = Cic.substitution
-let cic_apply_subst = CicMetaSubst.apply_subst
-let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
-let cic_ppsubst = CicMetaSubst.ppsubst
-let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
-let cic_flatten_subst subst =
-    List.map
-      (fun (i, (context, term, ty)) ->
-         let context = (* cic_apply_subst_context subst*) context in
-         let term = cic_apply_subst subst term in
-         let ty = cic_apply_subst subst ty in  
-         (i, (context, term, ty))) subst
-let rec cic_lookup_subst meta subst =
-  match meta with
-  | Cic.Meta (i, _) -> (
-      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
-      in cic_lookup_subst t subst 
-      with Not_found -> meta
-    )
-  | _ -> meta
-;;
-
-let cic_merge_subst_if_possible s1 s2 =
-  let already_in = Hashtbl.create 13 in
-  let rec aux acc = function
-    | ((i,_,x) as s)::tl ->
-        (try 
-          let x' = Hashtbl.find already_in i in
-          if x = x' then aux acc tl else None
-        with
-        | Not_found -> 
-            Hashtbl.add already_in i x;
-            aux (s::acc) tl)
-    | [] -> Some acc 
-  in  
-    aux [] (s1@s2)
-;;
-
-(******** NAIF substitution **************************************************)
-(* 
- * naif version of apply subst; the local context of metas is ignored;
- * we assume the substituted term must be lifted according to the nesting
- * depth of the meta. 
- * Alternatively, we could used implicit instead of metas 
- *)
-
-type naif_substitution = (int * Cic.term) list 
-
-let naif_apply_subst subst term =
- let rec aux k t =
-   match t with
-       Cic.Rel _ -> t
-     | Cic.Var (uri,exp_named_subst) -> 
-         let exp_named_subst' =
-           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-         in
-           Cic.Var (uri, exp_named_subst')
-    | Cic.Meta (i, l) -> 
-        (try
-          aux k (CicSubstitution.lift k (List.assoc i subst)) 
-         with Not_found -> t)
-    | Cic.Sort _
-    | Cic.Implicit _ -> t
-    | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
-    | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
-    | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
-    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
-    | Cic.Appl [] -> assert false
-    | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
-    | Cic.Const (uri,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-        in
-          if exp_named_subst' != exp_named_subst then
-            Cic.Const (uri, exp_named_subst')
-          else
-            t (* TODO: provare a mantenere il piu' possibile sharing *)
-    | Cic.MutInd (uri,typeno,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-        in
-          Cic.MutInd (uri,typeno,exp_named_subst')
-    | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-        let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-        in
-          Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | Cic.MutCase (sp,i,outty,t,pl) ->
-        let pl' = List.map (aux k) pl in
-          Cic.MutCase (sp, i, aux k outty, aux k t, pl')
-    | Cic.Fix (i, fl) ->
-        let len = List.length fl in
-        let fl' =
-         List.map 
-           (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
-        in
-          Cic.Fix (i, fl')
-    | Cic.CoFix (i, fl) ->
-        let len = List.length fl in
-        let fl' =
-          List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
-        in
-          Cic.CoFix (i, fl')
-in
-  aux 0 term
-;;
-
-(* naif version of apply_subst_metasenv: we do not apply the 
-substitution to the context *)
-
-let naif_apply_subst_metasenv subst metasenv =
-  List.map
-    (fun (n, context, ty) ->
-      (n, context, naif_apply_subst subst ty))
-    (List.filter
-      (fun (i, _, _) -> not (List.mem_assoc i subst))
-      metasenv)
-
-let naif_ppsubst names subst =
-  "{" ^ String.concat "; "
-    (List.map
-      (fun (idx, t) ->
-         Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
-    subst) ^ "}"
-;;
-
-let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
-
-let naif_flatten_subst subst = 
-  List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
-;;
-
-let rec naif_lookup_subst meta subst =
-  match meta with
-    | Cic.Meta (i, _) ->
-        (try
-          naif_lookup_subst (List.assoc i subst) subst
-        with
-            Not_found -> meta)
-    | _ -> meta
-;;
-
-let naif_merge_subst_if_possible s1 s2 =
-  let already_in = Hashtbl.create 13 in
-  let rec aux acc = function
-    | ((i,x) as s)::tl ->
-        (try 
-          let x' = Hashtbl.find already_in i in
-          if x = x' then aux acc tl else None
-        with
-        | Not_found -> 
-            Hashtbl.add already_in i x;
-            aux (s::acc) tl)
-    | [] -> Some acc 
-  in  
-    aux [] (s1@s2)
-;;
-
-(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
-
-type substitution = naif_substitution
-let apply_subst = naif_apply_subst
-let apply_subst_metasenv = naif_apply_subst_metasenv
-let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
-let buildsubst = naif_buildsubst
-let flatten_subst = naif_flatten_subst
-let lookup_subst = naif_lookup_subst
-
-(* filter out from metasenv the variables in substs *)
-let filter subst metasenv =
-  List.filter
-    (fun (m, _, _) ->
-         try let _ = List.find (fun (i, _) -> m = i) subst in false
-         with Not_found -> true)
-    metasenv
-;;
-
-let is_in_subst i subst = List.mem_assoc i subst;;
-  
-let merge_subst_if_possible = naif_merge_subst_if_possible;;
-
-let empty_subst = [];;
-
-(********* EQUALITY **********************************************************)
-
 type rule = SuperpositionRight | SuperpositionLeft | Demodulation
 type uncomparable = int -> int 
 type equality =
@@ -225,21 +37,11 @@ type equality =
      Utils.comparison) * (* ordering *)  
     Cic.metasenv  *      (* environment for metas *)
     int                  (* id *)
-and proof = new_proof * old_proof 
-
-and new_proof = 
+and proof = 
   | Exact of Cic.term
-  | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)  
-and old_proof =
-  | NoProof (* term is the goal missing a proof *)
-  | BasicProof of substitution * Cic.term
-  | ProofBlock of
-      substitution * UriManager.uri *
-        (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
-  | ProofGoalBlock of old_proof * old_proof 
-  | ProofSymBlock of Cic.term list * old_proof
-  | SubProof of Cic.term * int * old_proof
-and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+  | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term) 
+            (* subst, (rule,eq1, eq2,predicate) *)  
+and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
 
 (* globals *)
@@ -257,75 +59,65 @@ let reset () =
 
 let uncomparable = fun _ -> 0
 
-let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
+let mk_equality (weight,p,(ty,l,r,o),m) =
   let id = freshid () in
-  let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
+  let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
   Hashtbl.add id_to_eq id eq;
   eq
 ;;
 
+let mk_tmp_equality (weight,(ty,l,r,o),m) =
+  let id = -1 in
+  uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id
+;;
+
+
 let open_equality (_,weight,proof,(ty,l,r,o),m,id) = 
   (weight,proof,(ty,l,r,o),m,id)
 
+let string_of_rule = function
+  | SuperpositionRight -> "SupR"
+  | SuperpositionLeft -> "SupL"
+  | Demodulation -> "Demod"
+;;
+
 let string_of_equality ?env eq =
   match env with
   | None ->
-      let w, _, (ty, left, right, o), _ , id = open_equality eq in
-      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" 
+      let w, _, (ty, left, right, o), m , id = open_equality eq in
+      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" 
               id w (CicPp.ppterm ty)
               (CicPp.ppterm left) 
               (Utils.string_of_comparison o) (CicPp.ppterm right)
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   | Some (_, context, _) -> 
       let names = Utils.names_of_context context in
-      let w, _, (ty, left, right, o), _ , id = open_equality eq in
-      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" 
+      let w, _, (ty, left, right, o), m , id = open_equality eq in
+      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" 
               id w (CicPp.pp ty names)
               (CicPp.pp left names) (Utils.string_of_comparison o)
               (CicPp.pp right names)
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
 ;;
 
 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
   Pervasives.compare s1 s2
 ;;
 
-let rec string_of_proof_old ?(names=[]) = function
-  | NoProof -> "NoProof " 
-  | BasicProof (s, t) -> "BasicProof(" ^ 
-      ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
-  | SubProof (t, i, p) ->
-      Printf.sprintf "SubProof(%s, %s, %s)"
-        (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
-  | ProofSymBlock (_,p) -> 
-      Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
-  | ProofBlock (subst, _, _, _ ,(_,eq),old) -> 
-      let _,(_,p),_,_,_ = open_equality eq in 
-      "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
-      string_of_proof_old p ^ ")"
-  | ProofGoalBlock (p1, p2) ->
-      Printf.sprintf "ProofGoalBlock(%s, %s)"
-        (string_of_proof_old p1) (string_of_proof_old p2)
-;;
-
-
 let proof_of_id id =
   try
-    let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
-      p,m,l,r
+    let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+      p,l,r
   with
       Not_found -> assert false
 
 
-let string_of_proof_new ?(names=[]) p gp = 
-  let str_of_rule = function
-    | SuperpositionRight -> "SupR"
-    | SuperpositionLeft -> "SupL"
-    | Demodulation -> "Demod"
-  in
+let string_of_proof ?(names=[]) p gp = 
   let str_of_pos = function
     | Utils.Left -> "left"
     | Utils.Right -> "right"
   in
-  let fst4 (x,_,_,_) = x in
+  let fst3 (x,_,_) = x in
   let rec aux margin name = 
     let prefix = String.make margin ' ' ^ name ^ ": " in function 
     | Exact t -> 
@@ -333,27 +125,47 @@ let string_of_proof_new ?(names=[]) p gp =
           prefix (CicPp.pp t names)
     | Step (subst,(rule,eq1,(pos,eq2),pred)) -> 
         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
-          prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
+          prefix (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
           (CicPp.pp pred names)^ 
-        aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^ 
-        aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2)) 
+        aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ 
+        aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) 
   in
   aux 0 "" p ^ 
   String.concat "\n" 
     (List.map 
-      (fun (pos,i,s,t) -> 
+      (fun (r,pos,i,s,t) -> 
         (Printf.sprintf 
-          "GOAL: %s %d %s %s\n" 
-            (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^ 
-        aux 1 (Printf.sprintf "%d " i) (fst4 (proof_of_id i)))
+          "GOAL: %s %s %d %s %s\n" (string_of_rule r)
+            (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ 
+        aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
       gp)
 ;;
 
-let ppsubst = ppsubst ~names:[]
+let rec depend eq id seen =
+  let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
+  if List.mem ideq seen then 
+    false,seen
+  else
+    if id = ideq then 
+      true,seen
+    else  
+      match p with
+      | Exact _ -> false,seen
+      | Step (_,(_,id1,(_,id2),_)) ->
+          let seen = ideq::seen in
+          let eq1 = Hashtbl.find id_to_eq id1 in
+          let eq2 = Hashtbl.find id_to_eq id2 in  
+          let b1,seen = depend eq1 id seen in
+          if b1 then b1,seen else depend eq2 id seen
+;;
+
+let depend eq id = fst (depend eq id []);;
+
+let ppsubst = Subst.ppsubst ~names:[];;
 
 (* returns an explicit named subst and a list of arguments for sym_eq_URI *)
-let build_ens_for_sym_eq sym_eq_URI termlist =
-  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
+let build_ens uri termlist =
+  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
   match obj with
   | Cic.Constant (_, _, _, uris, _) ->
       assert (List.length uris <= List.length termlist);
@@ -368,184 +180,607 @@ let build_ens_for_sym_eq sym_eq_URI termlist =
   | _ -> assert false
 ;;
 
-let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
-  let rec do_build_proof proof = 
-    match proof with
-    | NoProof ->
-        Printf.fprintf stderr "WARNING: no proof!\n";
-        noproof
-    | BasicProof (s,term) -> apply_subst s term
-    | ProofGoalBlock (proofbit, proof) ->
-        print_endline "found ProofGoalBlock, going up...";
-        do_build_goal_proof proofbit proof
-    | ProofSymBlock (termlist, proof) ->
-        let proof = do_build_proof proof in
-        let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
-        Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
-    | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
-        let t' = Cic.Lambda (name, ty, bo) in
-        let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
-        let proof' = do_build_proof proof in
-        let eqproof = do_build_proof eqproof in
-        let what, other =
-          if pos = Utils.Left then what, other else other, what
-        in
-        apply_subst subst
-          (Cic.Appl [Cic.Const (eq_URI, []); ty;
-                     what; t'; eqproof; other; proof'])
-    | SubProof (term, meta_index, proof) ->
-        let proof = do_build_proof proof in
-        let eq i = function
-          | Cic.Meta (j, _) -> i = j
-          | _ -> false
+let mk_sym uri ty t1 t2 p =
+  let ens, args =  build_ens uri [ty;t1;t2;p] in
+    Cic.Appl (Cic.Const(uri, ens) :: args)
+;;
+
+let mk_trans uri ty t1 t2 t3 p12 p23 =
+  let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
+    Cic.Appl (Cic.Const (uri, ens) :: args)
+;;
+
+let mk_eq_ind uri ty what pred p1 other p2 =
+ Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
+;;
+
+let p_of_sym ens tl =
+  let args = List.map snd ens @ tl in
+  match args with 
+    | [_;_;_;p] -> p 
+    | _ -> assert false 
+;;
+
+let open_trans ens tl =
+  let args = List.map snd ens @ tl in
+  match args with 
+    | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
+    | _ -> assert false   
+;;
+
+let open_sym ens tl =
+  let args = List.map snd ens @ tl in
+  match args with 
+    | [ty;l;r;p] -> ty,l,r,p
+    | _ -> assert false   
+;;
+
+let open_eq_ind args =
+  match args with 
+  | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
+  | _ -> assert false   
+;;
+
+let open_pred pred =
+  match pred with 
+  | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) 
+     when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
+  | _ -> prerr_endline (CicPp.ppterm pred); assert false   
+;;
+
+let is_not_fixed t =
+   CicSubstitution.subst (Cic.Implicit None) t <>
+   CicSubstitution.subst (Cic.Rel 1) t
+;;
+
+
+let canonical t = 
+  let rec remove_refl t =
+    match t with
+    | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
+          when LibraryObjects.is_trans_eq_URI uri_trans ->
+          let ty,l,m,r,p1,p2 = open_trans ens tl in
+            (match p1,p2 with
+              | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 -> 
+                  remove_refl p2
+              | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] -> 
+                  remove_refl p1
+              | _ -> Cic.Appl (List.map remove_refl args))
+    | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
+    | Cic.LetIn (name,bo,rest) ->
+        Cic.LetIn (name,remove_refl bo,remove_refl rest)
+    | _ -> t
+  in
+  let rec canonical t =
+    match t with
+      | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
+      | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
+          when LibraryObjects.is_sym_eq_URI uri_sym ->
+          (match p_of_sym ens tl with
+             | Cic.Appl ((Cic.Const(uri,ens))::tl)
+                 when LibraryObjects.is_sym_eq_URI uri -> 
+                   canonical (p_of_sym ens tl)
+             | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+                 when LibraryObjects.is_trans_eq_URI uri_trans ->
+                 let ty,l,m,r,p1,p2 = open_trans ens tl in
+                   mk_trans uri_trans ty r m l 
+                     (canonical (mk_sym uri_sym ty m r p2)) 
+                     (canonical (mk_sym uri_sym ty l m p1))
+             | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl) 
+                 when LibraryObjects.is_eq_ind_URI uri_ind || 
+                      LibraryObjects.is_eq_ind_r_URI uri_ind ->
+                 let ty, what, pred, p1, other, p2 =
+                   match tl with
+                   | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
+                   | _ -> assert false
+                 in
+                 let pred,l,r = 
+                   match pred with
+                   | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
+                       when LibraryObjects.is_eq_URI uri ->
+                         Cic.Lambda 
+                           (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
+                   | _ -> 
+                       prerr_endline (CicPp.ppterm pred);
+                       assert false
+                 in
+                 let l = CicSubstitution.subst what l in
+                 let r = CicSubstitution.subst what r in
+                 Cic.Appl 
+                   [he;ty;what;pred;
+                    canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+             | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
+                 when LibraryObjects.is_eq_URI uri -> t
+             | _ -> Cic.Appl (List.map canonical args))
+      | Cic.Appl l -> Cic.Appl (List.map canonical l)
+      | _ -> t
+  in
+  remove_refl (canonical t)
+;;
+  
+let ty_of_lambda = function
+  | Cic.Lambda (_,ty,_) -> ty
+  | _ -> assert false 
+;;
+
+let compose_contexts ctx1 ctx2 = 
+  ProofEngineReduction.replace_lifting 
+    ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+;;
+
+let put_in_ctx ctx t = 
+  ProofEngineReduction.replace_lifting
+    ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
+;;
+
+let mk_eq uri ty l r =
+  Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
+;;
+
+let mk_refl uri ty t = 
+  Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
+;;
+
+let open_eq = function 
+  | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri ->
+      uri, ty, l ,r
+  | _ -> assert false
+;;
+
+let contextualize uri ty left right t = 
+  let hole = Cic.Implicit (Some `Hole) in
+  (* aux [uri] [ty] [left] [right] [ctx] [t] 
+   * 
+   * the parameters validate this invariant  
+   *   t: eq(uri) ty left right
+   * that is used only by the base case
+   *
+   * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
+   *)
+    let rec aux uri ty left right ctx_d = function
+      | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
+        when LibraryObjects.is_sym_eq_URI uri_sym  ->
+          let ty,l,r,p = open_sym ens tl in
+          mk_sym uri_sym ty l r (aux uri ty l r ctx_d p)
+      | Cic.LetIn (name,body,rest) ->
+          (* we should go in body *)
+          Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
+      | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
+        when LibraryObjects.is_eq_ind_URI uri_ind || 
+             LibraryObjects.is_eq_ind_r_URI uri_ind ->
+          let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+          let ty2,eq,lp,rp = open_pred pred in 
+          let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in
+          let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+          let is_not_fixed_lp = is_not_fixed lp in
+          let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
+          (* extract the context and the fixed term from the predicate *)
+          let m, ctx_c = 
+            let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
+            (* they were under a lambda *)
+            let m =  CicSubstitution.subst (Cic.Implicit None) m in
+            let ctx_c = CicSubstitution.subst hole ctx_c in
+            m, ctx_c          
+          in
+          (* create the compound context and put the terms under it *)
+          let ctx_dc = compose_contexts ctx_d ctx_c in
+          let dc_what = put_in_ctx ctx_dc what in
+          let dc_other = put_in_ctx ctx_dc other in
+          (* m is already in ctx_c so it is put in ctx_d only *)
+          let d_m = put_in_ctx ctx_d m in
+          (* we also need what in ctx_c *)
+          let c_what = put_in_ctx ctx_c what in
+          (* now put the proofs in the compound context *)
+          let p1 = (* p1: dc_what = d_m *)
+            if is_not_fixed_lp then 
+              aux uri ty1 c_what m ctx_d p1 
+            else
+              mk_sym uri_sym ty d_m dc_what
+                (aux uri ty1 m c_what ctx_d p1)
+          in
+          let p2 = (* p2: dc_other = dc_what *)
+            if avoid_eq_ind then
+              mk_sym uri_sym ty dc_what dc_other
+                (aux uri ty1 what other ctx_dc p2)
+            else
+              aux uri ty1 other what ctx_dc p2
+          in
+          (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
+             if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
+          let a,b,c,paeqb,pbeqc =
+            if is_not_fixed_lp then
+              dc_other,dc_what,d_m,p2,p1
+            else
+              d_m,dc_what,dc_other,
+                (mk_sym uri_sym ty dc_what d_m p1),
+                (mk_sym uri_sym ty dc_other dc_what p2)
+          in
+          mk_trans uri_trans ty a b c paeqb pbeqc
+    | t -> 
+        let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+        let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
+        let pred = 
+          (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
+          let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in
+          let l = 
+            let ctx_d = CicSubstitution.lift 1 ctx_d in
+            put_in_ctx ctx_d (Cic.Rel 1)
+          in
+          let lty = CicSubstitution.lift 1 ty in 
+          Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
         in
-        ProofEngineReduction.replace
-          ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
+        let d_left = put_in_ctx ctx_d left in
+        let d_right = put_in_ctx ctx_d right in
+        let refl_eq = mk_refl uri ty d_left in
+        mk_sym uri_sym ty d_right d_left
+          (mk_eq_ind uri_ind ty left pred refl_eq right t)
+  in
+  aux uri ty left right hole t
+;;
+
+let contextualize_rewrites t ty = 
+  let eq,ty,l,r = open_eq ty in
+  contextualize eq ty l r t
+;;
+
+let add_subst subst =
+  function
+    | Exact t -> Exact (Subst.apply_subst subst t)
+    | Step (s,(rule, id1, (pos,id2), pred)) -> 
+	Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+;;
+	
+let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
+  let p1 = Subst.apply_subst_lift lift subst p1 in
+  let p2 = Subst.apply_subst_lift lift subst p2 in
+  let l  = CicSubstitution.lift lift l in
+  let l = Subst.apply_subst_lift lift subst l in
+  let r  = CicSubstitution.lift lift r in
+  let r = Subst.apply_subst_lift lift subst r in
+  let pred = CicSubstitution.lift lift pred in
+  let pred = Subst.apply_subst_lift lift subst pred in
+  let ty,body = 
+    match pred with
+      | Cic.Lambda (_,ty,body) -> ty,body 
+      | _ -> assert false
+  in
+  let what, other = 
+    if pos = Utils.Left then l,r else r,l
+  in
+  let p =
+    match pos with
+      | Utils.Left ->
+        mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
+      | Utils.Right ->
+        mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
+  in
+  if sym then
+    let uri,pl,pr = 
+      let eq,_,pl,pr = open_eq body in
+      LibraryObjects.sym_eq_URI ~eq, pl, pr
+    in
+    let l = CicSubstitution.subst other pl in
+    let r = CicSubstitution.subst other pr in
+    mk_sym uri ty l r p
+  else
+    p
+;;
+
+let parametrize_proof p l r ty = 
+  let parameters = CicUtil.metas_of_term p 
+@ CicUtil.metas_of_term l 
+@ CicUtil.metas_of_term r
+in (* ?if they are under a lambda? *)
+  let parameters = 
+    HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
+  in
+  let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in 
+  let with_what, lift_no = 
+    List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1) 
+  in
+  let p = CicSubstitution.lift (lift_no-1) p in
+  let p = 
+    ProofEngineReduction.replace_lifting
+    ~equality:(fun t1 t2 -> 
+      match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
+    ~what ~with_what ~where:p
+  in
+  let ty_of_m _ = ty (*function 
+    | Cic.Meta (i,_) -> List.assoc i menv 
+    | _ -> assert false *)
+  in
+  let args, proof,_ = 
+    List.fold_left 
+      (fun (instance,p,n) m -> 
+        (instance@[m],
+        Cic.Lambda 
+          (Cic.Name ("x"^string_of_int n),
+          CicSubstitution.lift (lift_no - n - 1) (ty_of_m m),
+          p),
+        n+1)) 
+      ([Cic.Rel 1],p,1) 
+      what
+  in
+  let instance = match args with | [x] -> x | _ -> Cic.Appl args in
+  proof, instance
+;;
 
-  and do_build_goal_proof proofbit proof =
+let wfo goalproof proof id =
+  let rec aux acc id =
+    let p,_,_ = proof_of_id id in
+    match p with
+    | Exact _ -> if (List.mem id acc) then acc else id :: acc
+    | Step (_,(_,id1, (_,id2), _)) -> 
+        let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
+        let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
+        id :: acc
+  in
+  let acc = 
     match proof with
-    | ProofGoalBlock (pb, p) ->
-        do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
-    | _ -> do_build_proof (replace_proof proofbit proof)
-
-  and replace_proof newproof = function
-    | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
-        let eqproof' = replace_proof newproof eqproof in
-        ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
-    | ProofGoalBlock (pb, p) ->
-        let pb' = replace_proof newproof pb in
-        ProofGoalBlock (pb', p)
-    | BasicProof _ -> newproof
-    | SubProof (term, meta_index, p) ->
-        SubProof (term, meta_index, replace_proof newproof p)
-    | p -> p
-  in
-  do_build_proof proof 
-;;
-
-let build_proof_term_new proof =
-  let rec aux extra = function
-     | Exact term -> term
-     | Step (subst,(_, id1, (pos,id2), pred)) ->
-         let p,m1,_,_ = proof_of_id id1 in
-         let p1 = aux [] p in
-         let p,m3,l,r = proof_of_id id2 in 
-         let p2 = aux [] p in
-         let p1 = apply_subst subst p1 in
-         let p2 = apply_subst subst p2 in
-         let l = apply_subst subst l in
-         let r = apply_subst subst r in
-         let pred = apply_subst subst pred in
-         let ty = (* Cic.Implicit None *) 
+      | Exact _ -> [id]
+      | Step (_,(_,id1, (_,id2), _)) -> aux (aux [id] id1) id2
+  in 
+  List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof
+;;
+
+let string_of_id names id = 
+  if id = 0 then "" else 
+  try
+    let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
+    match p with
+    | Exact t -> 
+        Printf.sprintf "%d = %s: %s = %s [%s]" id
+          (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+    | Step (_,(step,id1, (_,id2), _) ) ->
+        Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
+          (string_of_rule step)
+          id1 id2 (CicPp.pp l names) (CicPp.pp r names)
+        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+  with
+      Not_found -> assert false
+
+let pp_proof names goalproof proof subst id initial_goal =
+  String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^ 
+  "\ngoal:\n   " ^ 
+    (String.concat "\n   " 
+      (fst (List.fold_right
+        (fun (r,pos,i,s,pred) (acc,g) -> 
+          let _,_,left,right = open_eq g in
+          let ty = 
+            match pos with 
+            | Utils.Left -> CicReduction.head_beta_reduce (Cic.Appl[pred;right])
+            | Utils.Right -> CicReduction.head_beta_reduce (Cic.Appl[pred;left])
+          in
+          let ty = Subst.apply_subst s ty in
+          ("("^ string_of_rule r ^ " " ^ string_of_int i^") -> "
+          ^ CicPp.pp ty names) :: acc,ty) goalproof ([],initial_goal)))) ^
+  "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst
+;;
+
+module OT = 
+  struct
+    type t = int
+    let compare = Pervasives.compare
+  end
+
+module M = Map.Make(OT)
+
+let rec find_deps m i = 
+  if M.mem i m then m
+  else 
+    let p,_,_ = proof_of_id i in
+    match p with
+    | Exact _ -> M.add i [] m
+    | Step (_,(_,id1,(_,id2),_)) -> 
+        let m = find_deps m id1 in
+        let m = find_deps m id2 in
+        M.add i (M.find id1 m @ M.find id2 m @ [id1;id2]) m
+;;
+
+let topological_sort l = 
+  (* build the partial order relation *)
+  let m = 
+    List.fold_left (fun m i -> find_deps m i)
+    M.empty l
+  in
+  let m = M.map (fun x -> Some x) m in
+  (* utils *)
+  let keys m = M.fold (fun i _ acc -> i::acc) m [] in
+  let split l m = List.filter (fun i -> M.find i m = Some []) l in
+  let purge l m = 
+    M.mapi 
+      (fun k v -> if List.mem k l then None else 
+         match v with
+         | None -> None
+         | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll)) 
+      m
+  in
+  let rec aux m = 
+      let keys = keys m in
+      let ok = split keys m in
+      let m = purge ok m in
+      ok @ (if ok = [] then [] else aux m)
+  in
+  aux m
+;;
+  
+
+(* returns the list of ids that should be factorized *)
+let get_duplicate_step_in_wfo l p =
+  let ol = List.rev l in
+  let h = Hashtbl.create 13 in
+  (* NOTE: here the n parameter is an approximation of the dependency 
+     between equations. To do things seriously we should maintain a 
+     dependency graph. This approximation is not perfect. *)
+  let add i = 
+    let p,_,_ = proof_of_id i in 
+    match p with 
+    | Exact _ -> true
+    | _ -> 
+        try 
+          let no = Hashtbl.find h i in
+          Hashtbl.replace h i (no+1);
+          false
+        with Not_found -> Hashtbl.add h i 1;true
+  in
+  let rec aux = function
+    | Exact _ -> ()
+    | Step (_,(_,i1,(_,i2),_)) -> 
+        let go_on_1 = add i1 in
+        let go_on_2 = add i2 in
+        if go_on_1 then aux (let p,_,_ = proof_of_id i1 in p);
+        if go_on_2 then aux (let p,_,_ = proof_of_id i2 in p)
+  in
+  aux p;
+  List.iter
+    (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id id in p))
+    ol;
+  (* now h is complete *)
+  let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
+  let proofs = List.filter (fun (_,c) -> c > 1) proofs in
+  topological_sort (List.map (fun (i,_) -> i) proofs)
+;;
+
+let build_proof_term h lift proof =
+  let proof_of_id aux id =
+    let p,l,r = proof_of_id id in
+    try List.assoc id h,l,r with Not_found -> aux p, l, r
+  in
+  let rec aux = function
+     | Exact term -> CicSubstitution.lift lift term
+     | Step (subst,(rule, id1, (pos,id2), pred)) ->
+         let p1,_,_ = proof_of_id aux id1 in
+         let p2,l,r = proof_of_id aux id2 in
+         let varname = 
+           match rule with
+           | SuperpositionRight -> Cic.Name ("SupR" ^ Utils.string_of_pos pos) 
+           | Demodulation -> Cic.Name ("DemEq"^ Utils.string_of_pos pos)
+           | _ -> assert false
+         in
+         let pred = 
            match pred with
-           | Cic.Lambda (_,ty,_) -> ty 
+           | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
            | _ -> assert false
          in
-         let what, other = (* Cic.Implicit None, Cic.Implicit None *)
-           if pos = Utils.Left then l,r else r,l
+         let p =   build_proof_step lift subst p1 p2 pos l r pred in
+(*         let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
+           if not cond then
+             prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
+           assert cond;*)
+           p
+  in
+   aux proof
+;;
+
+let build_goal_proof l initial ty se =
+  let se = List.map (fun i -> Cic.Meta (i,[])) se in 
+  let lets = get_duplicate_step_in_wfo l initial in
+  let letsno = List.length lets in
+  let _,mty,_,_ = open_eq ty in
+  let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l 
+  in
+  let lets,_,h = 
+    List.fold_left
+      (fun (acc,n,h) id -> 
+        let p,l,r = proof_of_id id in
+        let cic = build_proof_term h n p in
+        let real_cic,instance = 
+          parametrize_proof cic l r (CicSubstitution.lift n mty)
+        in
+        let h = (id, instance)::lift_list h in
+        acc@[id,real_cic],n+1,h) 
+      ([],0,[]) lets
+  in
+  let proof,se = 
+    let rec aux se current_proof = function
+      | [] -> current_proof,se
+      | (rule,pos,id,subst,pred)::tl ->
+          let p,l,r = proof_of_id id in
+           let p = build_proof_term h letsno p in
+           let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+         let varname = 
+           match rule with
+           | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos) 
+           | Demodulation -> Cic.Name ("DemG"^ Utils.string_of_pos pos)
+           | _ -> assert false
          in
-         let eq_URI =
-           match pos with 
-           | Utils.Left -> Utils.eq_ind_URI () 
-           | Utils.Right ->  Utils.eq_ind_r_URI ()
-         in 
-         (Cic.Appl [
-           Cic.Const (eq_URI, []); 
-           ty; what; pred; p1; other; p2]) 
-  in
-   aux [] proof
-
-let build_goal_proof l refl=
-  let proof, subst = 
-   List.fold_left 
-   (fun  (current_proof,current_subst) (pos,id,subst,pred) -> 
-      let p,m,l,r = proof_of_id id in
-      let p = build_proof_term_new p in
-      let p = apply_subst subst p in
-      let l = apply_subst subst l in
-      let r = apply_subst subst r in
-      let pred = apply_subst subst pred in
-      let ty = (* Cic.Implicit None *) 
-        match pred with
-        | Cic.Lambda (_,ty,_) -> ty 
-        | _ -> assert false
-      in
-      let what, other = (* Cic.Implicit None, Cic.Implicit None *)
-        if pos = Utils.Right then l,r else r,l
-      in
-      let eq_URI =
-        match pos with
-          | Utils.Left -> Utils.eq_ind_r_URI ()
-          | Utils.Right ->  Utils.eq_ind_URI () 
-      in
-        ((Cic.Appl [Cic.Const (eq_URI, []);
-          ty; what; pred; current_proof; other; p]), subst @ current_subst))
-   (refl,[]) l
+         let pred = 
+           match pred with
+           | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
+           | _ -> assert false
+         in
+           let proof = 
+             build_proof_step letsno subst current_proof p pos l r pred
+           in
+           let proof,se = aux se proof tl in
+           Subst.apply_subst_lift letsno subst proof,
+           List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
+    in
+    aux se (build_proof_term h letsno initial) l
+  in
+  let n,proof = 
+    let initial = proof in
+    List.fold_right
+      (fun (id,cic) (n,p) -> 
+        n-1,
+        Cic.LetIn (
+          Cic.Name ("H"^string_of_int id),
+          cic, p))
+    lets (letsno-1,initial)
   in
-  proof
+    (proof,se)
+  (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+   se *)
 ;;
 
 let refl_proof ty term = 
   Cic.Appl 
     [Cic.MutConstruct 
-       (LibraryObjects.eq_URI (), 0, 1, []);
+       (Utils.eq_URI (), 0, 1, []);
        ty; term]
 ;;
 
-let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
+let metas_of_proof p =
+  let p = build_proof_term [] 0 p in
+  Utils.metas_of_term p
+;;
 
-let relocate newmeta menv =
-  let subst, metasenv, newmeta = 
+let relocate newmeta menv to_be_relocated =
+  let subst, newmetasenv, newmeta = 
     List.fold_right 
-      (fun (i, context, ty) (subst, menv, maxmeta) ->         
-        let irl = [] (*
-         CicMkImplicit.identity_relocation_list_for_metavariable context *)
-        in
-        let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
-        let newmeta = maxmeta, context, ty in
-        newsubst, newmeta::menv, maxmeta+1) 
-      menv ([], [], newmeta+1)
+      (fun i (subst, metasenv, maxmeta) ->         
+        let _,context,ty = CicUtil.lookup_meta i menv in
+        let irl = [] in
+        let newmeta = Cic.Meta(maxmeta,irl) in
+        let newsubst = Subst.buildsubst i context newmeta ty subst in
+        newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) 
+      to_be_relocated (Subst.empty_subst, [], newmeta+1)
   in
-  let metasenv = apply_subst_metasenv subst metasenv in
-  let subst = flatten_subst subst in
-  subst, metasenv, newmeta
+  let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
+  subst, menv, newmeta
 
 
 let fix_metas newmeta eq = 
-  let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
-  (* debug 
-  let _ , eq = 
-    fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
-  prerr_endline (string_of_equality eq); *)
-  let subst, metasenv, newmeta = relocate newmeta menv in
-  let ty = apply_subst subst ty in
-  let left = apply_subst subst left in
-  let right = apply_subst subst right in
+  let w, p, (ty, left, right, o), menv,_ = open_equality eq in
+  let to_be_relocated = 
+(* List.map (fun i ,_,_ -> i) menv *)
+    HExtlib.list_uniq 
+      (List.sort Pervasives.compare 
+         (Utils.metas_of_term left @ Utils.metas_of_term right)) 
+  in
+  let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
+  let ty = Subst.apply_subst subst ty in
+  let left = Subst.apply_subst subst left in
+  let right = Subst.apply_subst subst right in
   let fix_proof = function
-    | NoProof -> NoProof 
-    | BasicProof (subst',term) -> BasicProof (subst@subst',term)
-    | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
-        (*
-        let newsubst = 
-          List.map
-            (fun (i, (context, term, ty)) ->
-               let context = apply_subst_context subst context in
-               let term = apply_subst subst term in
-               let ty = apply_subst subst ty in  
-                 (i, (context, term, ty))) subst' in *)
-          ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
-    | p -> assert false
-  in
-  let fix_new_proof = function
-    | Exact p -> Exact (apply_subst subst p)
+    | Exact p -> Exact (Subst.apply_subst subst p)
     | Step (s,(r,id1,(pos,id2),pred)) -> 
-        Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
+        Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
   in
-  let new_p = fix_new_proof p1 in
-  let old_p = fix_proof p2 in
-  let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
-  (* debug prerr_endline (string_of_equality eq); *)
-  newmeta+1, eq  
+  let p = fix_proof p in
+  let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in
+  newmeta+1, eq'  
 
 exception NotMetaConvertible;;
 
@@ -677,21 +912,21 @@ let meta_convertibility t1 t2 =
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
-  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+  let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
   | _ -> false
 ;;
 
 let equality_of_term proof term =
-  let eq_uri = LibraryObjects.eq_URI () in
+  let eq_uri = Utils.eq_URI () in
   let iseq uri = UriManager.eq uri eq_uri in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
       let o = !Utils.compare_terms t1 t2 in
       let stat = (ty,t1,t2,o) in
       let w = Utils.compute_equality_weight stat in
-      let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
+      let e = mk_equality (w, Exact proof, stat,[]) in
       e
   | _ ->
       raise TermIsNotAnEquality
@@ -716,7 +951,7 @@ let term_of_equality equality =
   let argsno = List.length menv in
   let t =
     CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+      (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
   in
   snd (
     List.fold_right
@@ -732,3 +967,24 @@ let term_of_equality equality =
       menv (argsno, t))
 ;;
 
+let symmetric eq_ty l id uri m =
+  let eq = Cic.MutInd(uri,0,[]) in
+  let pred = 
+    Cic.Lambda (Cic.Name "Sym",eq_ty,
+     Cic.Appl [CicSubstitution.lift 1 eq ;
+               CicSubstitution.lift 1 eq_ty;
+               Cic.Rel 1;CicSubstitution.lift 1 l]) 
+  in
+  let prefl = 
+    Exact (Cic.Appl
+      [Cic.MutConstruct(uri,0,1,[]);eq_ty;l]) 
+  in
+  let id1 = 
+    let eq = mk_equality (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+    let (_,_,_,_,id) = open_equality eq in
+    id
+  in
+  Step(Subst.empty_subst,
+    (Demodulation,id1,(Utils.Left,id),pred))
+;;
+