+let build_proof_term equality =
+(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(* print_newline (); *)
+
+ let indent = ref 0 in
+
+ let rec do_build_proof proof =
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof!\n";
+(* (string_of_equality equality); *)
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofGoalBlock (proofbit, equality) ->
+ print_endline "found ProofGoalBlock, going up...";
+ let _, proof, _, _, _ = equality in
+ do_build_goal_proof proofbit proof
+ | ProofSymBlock (ens, proof) ->
+ let proof = do_build_proof proof in
+ Cic.Appl [
+ Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
+ proof
+ ]
+ | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) ->
+(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
+(* print_newline (); *)
+
+ let name, ty, eq_ty, left, right = t' in
+ let bo =
+ Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ eq_ty; left; right]
+ in
+ let t' = Cic.Lambda (name, ty, (* CicSubstitution.lift 1 *) bo) in
+ (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
+ (* (string_of_equality eq) (string_of_equality eq'); *)
+ (* print_newline (); *)
+
+(* let s = String.make !indent ' ' in *)
+(* incr indent; *)
+
+(* print_endline (s ^ "build proof'------------"); *)
+
+ let proof' =
+ let _, proof', _, _, _ = eq in
+ do_build_proof proof'
+ in
+(* print_endline (s ^ "END proof'"); *)
+
+(* print_endline (s ^ "build eqproof-----------"); *)
+
+ let eqproof = do_build_proof eqproof in
+
+(* print_endline (s ^ "END eqproof"); *)
+(* decr indent; *)
+
+
+ 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'])
+
+ and do_build_goal_proof proofbit proof =
+(* match proofbit with *)
+(* | BasicProof _ -> do_build_proof proof *)
+(* | proofbit -> *)
+ match proof with
+ | ProofGoalBlock (pb, eq) ->
+ do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq))
+(* let _, proof, _, _, _ = eq in *)
+(* let newproof = replace_proof proofbit proof in *)
+(* do_build_proof newproof *)
+
+(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
+(* let eqproof' = replace_proof proofbit eqproof in *)
+(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
+ | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
+
+ and replace_proof newproof = function
+ | ProofBlock (subst, eq_URI, t', poseq, eqproof) ->
+ let uri = eq_URI in
+(* if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *)
+(* HelmLibraryObjects.Logic.eq_ind_r_URI *)
+(* else *)
+(* HelmLibraryObjects.Logic.eq_ind_URI *)
+(* in *)
+ let eqproof' = replace_proof newproof eqproof in
+ ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof')
+(* ProofBlock (subst, eq_URI, t', poseq, newproof) *)
+ | ProofGoalBlock (pb, equality) ->
+ let pb' = replace_proof newproof pb in
+ ProofGoalBlock (pb', equality)
+(* let w, proof, t, menv, args = equality in *)
+(* let proof' = replace_proof newproof proof in *)
+(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
+ | BasicProof _ -> newproof
+ | p -> p
+ in
+ let _, proof, _, _, _ = equality in
+ do_build_proof proof
+;;
+
+