+let prooftable = Hashtbl.create 2001;;
+
+let store_proof equality proof =
+ if not (Hashtbl.mem prooftable equality) then
+ Hashtbl.add prooftable equality proof
+;;
+
+
+let delete_proof equality =
+(* Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
+(* print_newline (); *)
+ Hashtbl.remove prooftable equality
+;;
+
+
+let rec build_term_proof equality =
+(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(* print_newline (); *)
+ let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof for %s\n"
+ (string_of_equality equality);
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
+(* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
+(* (string_of_equality eq) (string_of_equality eq'); *)
+(* print_newline (); *)
+ let proof' = build_term_proof eq in
+ let eqproof = build_term_proof eq' in
+ let _, (ty, what, other, _), menv', args' = eq in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ CicMetaSubst.apply_subst subst
+ (Cic.Appl [Cic.Const (eq_URI, []); ty;
+ what; t'; eqproof; other; proof'])
+;;
+
+