+let rec build_term_proof equality =
+(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(* print_newline (); *)
+ let _, proof, _, _, _ = equality 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') ->
+ 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 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'])
+;;
+
+