diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
index fe951187703..afc40a7d4a0 100644
--- a/include/cvc5/cvc5_proof_rule.h
+++ b/include/cvc5/cvc5_proof_rule.h
@@ -156,7 +156,7 @@ enum ENUM(ProofRule) : uint32_t
    * where :math:`idr` is a MethodId identifier, which determines the kind of
    * rewriter to apply, e.g. Rewriter::rewrite. \endverbatim
    */
-  EVALUE(REWRITE),
+  EVALUE(MACRO_REWRITE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Builtin theory -- Evaluate**
@@ -315,17 +315,18 @@ enum ENUM(ProofRule) : uint32_t
 
   /**
    * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory lemma**
+   * **Trusted rule**
    *
    * .. math::
-   *   \inferrule{- \mid F, tid}{F}
+   *   \inferrule{F_1 \dots F_n \mid tid, F, ...}{F}
    *
-   * where :math:`F` is a (T-valid) theory lemma generated by theory with
-   * TheoryId :math:`tid`. This is a "coarse-grained" rule that is used as a
-   * placeholder if a theory did not provide a proof for a lemma or conflict.
+   * where :math:`tid` is an identifier and :math:`F` is a formula. This rule
+   * is used when a formal justification of an inference step cannot be provided.
+   * The formulas :math:`F_1 \dots F_n` refer to a set of formulas that
+   * entail :math:`F`, which may or may not be provided.
    * \endverbatim
    */
-  EVALUE(THEORY_LEMMA),
+  EVALUE(TRUST),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Trusted rules -- Theory rewrite**
@@ -343,146 +344,7 @@ enum ENUM(ProofRule) : uint32_t
    * bound variables that are not guaranteed to be consistent on each call.
    * \endverbatim
    */
-  EVALUE(THEORY_REWRITE),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory preprocessing**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t =
-   * \texttt{Theory::ppRewrite}(t)` for some theory. \endverbatim
-   */
-  EVALUE(THEORY_PREPROCESS),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory preprocessing**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` was added as a new assertion by theory preprocessing from
-   * the theory with identifier tid.
-   * \endverbatim
-   */
-  EVALUE(THEORY_PREPROCESS_LEMMA),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Preprocessing**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t = t'` where :math:`t`
-   * was replaced by :math:`t'` based on some preprocessing pass, or otherwise
-   * :math:`F` was added as a new assertion by some preprocessing pass.
-   * \endverbatim
-   */
-  EVALUE(PREPROCESS),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Preprocessing new assertion**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` was added as a new assertion by some preprocessing pass.
-   * \endverbatim
-   */
-  EVALUE(PREPROCESS_LEMMA),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory expand definitions**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t = t'` where :math:`t`
-   * was replaced by :math:`t'` based on theory expand definitions. \endverbatim
-   */
-  EVALUE(THEORY_EXPAND_DEF),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Witness term axiom**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an existential ``(exists ((x T)) (P x))`` used for
-   * introducing a witness term ``(witness ((x T)) (P x))``. \endverbatim
-   */
-  EVALUE(WITNESS_AXIOM),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-replayable rewriting**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality `t = t'` that holds by a form of rewriting
-   * that could not be replayed during proof postprocessing. \endverbatim
-   */
-  EVALUE(TRUST_REWRITE),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-supported flattening rewrite **
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality `t = t'` where both `t` and `t'` are
-   * applications of associative operators but the rewriter does not support
-   * flattening them to the same normal form. \endverbatim
-   */
-  EVALUE(TRUST_FLATTENING_REWRITE),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-replayable substitution**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality :math:`t = t'` that holds by a form of
-   * substitution that could not be replayed during proof postprocessing.
-   * \endverbatim
-   */
-  EVALUE(TRUST_SUBS),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-replayable substitution map**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality :math:`t = t'` that holds by a form of
-   * substitution that could not be determined by the TrustSubstitutionMap. This
-   * inference may contain possibly multiple children corresponding to the
-   * formulas used to derive the substitution. \endverbatim
-   */
-  EVALUE(TRUST_SUBS_MAP),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Solved equality**
-   *
-   * .. math::
-   *   \inferrule{F' \mid F}{F}
-   *
-   * where :math:`F` is a solved equality of the form :math:`x = t` derived as
-   * the solved form of :math:`F'`. \endverbatim
-   */
-  EVALUE(TRUST_SUBS_EQ),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Theory-specific inference**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is a fact derived by a theory-specific inference.
-   * \endverbatim
-   */
-  EVALUE(THEORY_INFERENCE),
+  EVALUE(TRUST_THEORY_REWRITE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **SAT Refutation for assumption-based unsat cores**
@@ -1276,7 +1138,7 @@ enum ENUM(ProofRule) : uint32_t
 
   /**
    * \verbatim embed:rst:leading-asterisk
-   * **Bit-vectors -- Bitblast**
+   * **Bit-vectors -- (Macro) Bitblast**
    *
    * .. math::
    *
@@ -1288,7 +1150,7 @@ enum ENUM(ProofRule) : uint32_t
    * strategies defined in ``theory/bv/bitblast/bitblast_strategies_template.h``.
    * \endverbatim
    */
-  EVALUE(BV_BITBLAST),
+  EVALUE(MACRO_BV_BITBLAST),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bit-vectors -- Bitblast bit-vector constant, variable, and terms**
@@ -1459,19 +1321,6 @@ enum ENUM(ProofRule) : uint32_t
    * \endverbatim
    */
   EVALUE(ALPHA_EQUIV),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Quantifiers -- (Trusted) quantifiers preprocessing**
-   *
-   * .. math::
-   *
-   *   \inferrule{?\mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t =
-   * \texttt{QuantifiersPreprocess::preprocess(t)}`.
-   * \endverbatim
-   */
-  EVALUE(QUANTIFIERS_PREPROCESS),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Strings -- Core rules -- Concatenation equality**
@@ -1816,7 +1665,7 @@ enum ENUM(ProofRule) : uint32_t
   EVALUE(STRING_SEQ_UNIT_INJ),
   /**
    * \verbatim embed:rst:leading-asterisk
-   * **Strings -- (Trusted) String inference**
+   * **Strings -- (Macro) String inference**
    *
    * .. math::
    *
@@ -1826,7 +1675,7 @@ enum ENUM(ProofRule) : uint32_t
    * :math:`\texttt{strings::InferProofCons::convert}`.
    * \endverbatim
    */
-  EVALUE(STRING_INFERENCE),
+  EVALUE(MACRO_STRING_INFERENCE),
 
   /**
    * \verbatim embed:rst:leading-asterisk
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4d546c90933..7da0ea9562d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -212,6 +212,8 @@ libcvc5_add_sources(
   proof/proof_step_buffer.h
   proof/resolution_proofs_util.cpp
   proof/resolution_proofs_util.h
+  proof/trust_id.cpp
+  proof/trust_id.h
   proof/trust_node.cpp
   proof/trust_node.h
   proof/theory_proof_step_buffer.cpp
diff --git a/src/api/cpp/cvc5_proof_rule.cpp b/src/api/cpp/cvc5_proof_rule.cpp
index e67aa368a59..0918f1e1483 100644
--- a/src/api/cpp/cvc5_proof_rule.cpp
+++ b/src/api/cpp/cvc5_proof_rule.cpp
@@ -27,7 +27,7 @@ const char* toString(ProofRule id)
     case ProofRule::ASSUME: return "ASSUME";
     case ProofRule::SCOPE: return "SCOPE";
     case ProofRule::SUBS: return "SUBS";
-    case ProofRule::REWRITE: return "REWRITE";
+    case ProofRule::MACRO_REWRITE: return "MACRO_REWRITE";
     case ProofRule::EVALUATE: return "EVALUATE";
     case ProofRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
     case ProofRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
@@ -38,20 +38,8 @@ const char* toString(ProofRule id)
     case ProofRule::DSL_REWRITE: return "DSL_REWRITE";
     case ProofRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
     //================================================= Trusted rules
-    case ProofRule::THEORY_LEMMA: return "THEORY_LEMMA";
-    case ProofRule::THEORY_REWRITE: return "THEORY_REWRITE";
-    case ProofRule::PREPROCESS: return "PREPROCESS";
-    case ProofRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
-    case ProofRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
-    case ProofRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
-    case ProofRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF";
-    case ProofRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
-    case ProofRule::TRUST_REWRITE: return "TRUST_REWRITE";
-    case ProofRule::TRUST_FLATTENING_REWRITE: return "TRUST_FLATTENING_REWRITE";
-    case ProofRule::TRUST_SUBS: return "TRUST_SUBS";
-    case ProofRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
-    case ProofRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ";
-    case ProofRule::THEORY_INFERENCE: return "THEORY_INFERENCE";
+    case ProofRule::TRUST: return "TRUST";
+    case ProofRule::TRUST_THEORY_REWRITE: return "TRUST_THEORY_REWRITE";
     case ProofRule::SAT_REFUTATION: return "SAT_REFUTATION";
     //================================================= Boolean rules
     case ProofRule::RESOLUTION: return "RESOLUTION";
@@ -126,7 +114,7 @@ const char* toString(ProofRule id)
     case ProofRule::ARRAYS_EXT: return "ARRAYS_EXT";
     case ProofRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND";
     //================================================= Bit-Vector rules
-    case ProofRule::BV_BITBLAST: return "BV_BITBLAST";
+    case ProofRule::MACRO_BV_BITBLAST: return "MACRO_BV_BITBLAST";
     case ProofRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP";
     case ProofRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
     //================================================= Datatype rules
@@ -140,7 +128,6 @@ const char* toString(ProofRule id)
     case ProofRule::SKOLEMIZE: return "SKOLEMIZE";
     case ProofRule::INSTANTIATE: return "INSTANTIATE";
     case ProofRule::ALPHA_EQUIV: return "ALPHA_EQUIV";
-    case ProofRule::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS";
     //================================================= String rules
     case ProofRule::CONCAT_EQ: return "CONCAT_EQ";
     case ProofRule::CONCAT_UNIFY: return "CONCAT_UNIFY";
@@ -162,7 +149,7 @@ const char* toString(ProofRule id)
     case ProofRule::RE_ELIM: return "RE_ELIM";
     case ProofRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
     case ProofRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
-    case ProofRule::STRING_INFERENCE: return "STRING_INFERENCE";
+    case ProofRule::MACRO_STRING_INFERENCE: return "MACRO_STRING_INFERENCE";
     //================================================= Arith rules
     case ProofRule::MACRO_ARITH_SCALE_SUM_UB: return "MACRO_ARITH_SCALE_SUM_UB";
     case ProofRule::ARITH_SUM_UB: return "ARITH_SUM_UB";
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 60b944ed2cd..c583d0ff96a 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -197,7 +197,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
       //   rewrite( d_nodes[i] ^ n )
       // allocate a fresh proof which will act as the proof generator
       LazyCDProof* lcp = d_pppg->allocateHelperProof();
-      lcp->addLazyStep(n, pg, ProofRule::PREPROCESS);
+      lcp->addLazyStep(n, pg, TrustId::PREPROCESS);
       // if newConj was constructed by AND above, use AND_INTRO
       if (newConj != n)
       {
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index ea4a7e2b27a..b323e8d32a6 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -121,12 +121,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   // constant propagations
   std::shared_ptr<TrustSubstitutionMap> constantPropagations =
       std::make_shared<TrustSubstitutionMap>(
-          d_env, u, "NonClausalSimp::cprop", ProofRule::PREPROCESS_LEMMA);
+          d_env, u, "NonClausalSimp::cprop", TrustId::PREPROCESS_LEMMA);
   SubstitutionMap& cps = constantPropagations->get();
   // new substitutions
   std::shared_ptr<TrustSubstitutionMap> newSubstitutions =
       std::make_shared<TrustSubstitutionMap>(
-          d_env, u, "NonClausalSimp::newSubs", ProofRule::PREPROCESS_LEMMA);
+          d_env, u, "NonClausalSimp::newSubs", TrustId::PREPROCESS_LEMMA);
   SubstitutionMap& nss = newSubstitutions->get();
 
   size_t j = 0;
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 6b30091195e..c66ac64f32b 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -383,7 +383,7 @@ bool AletheProofPostprocessCallback::update(Node res,
 
       return success;
     }
-    case ProofRule::THEORY_REWRITE:
+    case ProofRule::TRUST_THEORY_REWRITE:
     {
       return addAletheStep(AletheRule::ALL_SIMPLIFY,
                            res,
diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp
index b68ea6d8987..609342eb713 100644
--- a/src/proof/conv_proof_generator.cpp
+++ b/src/proof/conv_proof_generator.cpp
@@ -75,7 +75,7 @@ void TConvProofGenerator::addRewriteStep(Node t,
                                          Node s,
                                          ProofGenerator* pg,
                                          bool isPre,
-                                         ProofRule trustId,
+                                         TrustId trustId,
                                          bool isClosed,
                                          uint32_t tctx)
 {
diff --git a/src/proof/conv_proof_generator.h b/src/proof/conv_proof_generator.h
index 8bb3a25a028..46538d94a6d 100644
--- a/src/proof/conv_proof_generator.h
+++ b/src/proof/conv_proof_generator.h
@@ -158,7 +158,7 @@ class TConvProofGenerator : protected EnvObj, public ProofGenerator
                       Node s,
                       ProofGenerator* pg,
                       bool isPre = false,
-                      ProofRule trustId = ProofRule::ASSUME,
+                      TrustId trustId = TrustId::NONE,
                       bool isClosed = false,
                       uint32_t tctx = 0);
   /** Same as above, for a single step */
diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index ced68d45285..cbf1f153b56 100644
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -25,6 +25,7 @@
 #include "proof/proof_checker.h"
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
+#include "proof/trust_id.h"
 #include "theory/builtin/proof_checker.h"
 
 namespace cvc5::internal {
@@ -397,7 +398,7 @@ ProofNodeClusterType DotPrinter::defineProofNodeType(const ProofNode* pn,
       return ProofNodeClusterType::CNF;
     }
     // If the first rule after a CNF is in the TL range
-    if (isTheoryLemma(rule))
+    if (isTheoryLemma(pn))
     {
       return ProofNodeClusterType::THEORY_LEMMA;
     }
@@ -460,9 +461,18 @@ inline bool DotPrinter::isSCOPE(const ProofRule& rule)
   return ProofRule::SCOPE == rule;
 }
 
-inline bool DotPrinter::isTheoryLemma(const ProofRule& rule)
+inline bool DotPrinter::isTheoryLemma(const ProofNode* pn)
 {
-  return rule == ProofRule::SCOPE || rule == ProofRule::THEORY_LEMMA
+  ProofRule rule = pn->getRule();
+  if (rule == ProofRule::TRUST)
+  {
+    TrustId tid;
+    if (getTrustId(pn->getArguments()[0], tid))
+    {
+      return tid == TrustId::THEORY_LEMMA;
+    }
+  }
+  return rule == ProofRule::SCOPE
          || (ProofRule::CNF_ITE_NEG3 < rule && rule < ProofRule::LFSC_RULE);
 }
 
@@ -501,7 +511,7 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
     }
   }
   // if th_rw, likewise
-  else if (r == ProofRule::THEORY_REWRITE)
+  else if (r == ProofRule::TRUST_THEORY_REWRITE)
   {
     // print the second argument
     theory::TheoryId id;
diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index b8cc13738c4..94bb3492e55 100644
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -194,7 +194,7 @@ class DotPrinter : protected EnvObj
    * @return The bool indicating whether the rule is for a theory lemma
    * range.
    */
-  inline bool isTheoryLemma(const ProofRule& rule);
+  inline bool isTheoryLemma(const ProofNode* pn);
 
   /** Verify if the rule is an ASSUME
    * @param rule The rule to be verified.
diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp
index d55b805b558..3cb750cb7b0 100644
--- a/src/proof/lazy_proof.cpp
+++ b/src/proof/lazy_proof.cpp
@@ -165,7 +165,7 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact)
 
 void LazyCDProof::addLazyStep(Node expected,
                               ProofGenerator* pg,
-                              ProofRule idNull,
+                              TrustId idNull,
                               bool isClosed,
                               const char* ctx,
                               bool forceOverwrite)
@@ -173,7 +173,7 @@ void LazyCDProof::addLazyStep(Node expected,
   if (pg == nullptr)
   {
     // null generator, should have given a proof rule
-    if (idNull == ProofRule::ASSUME)
+    if (idNull == TrustId::NONE)
     {
       Unreachable() << "LazyCDProof::addLazyStep: " << identify()
                     << ": failed to provide proof generator for " << expected;
@@ -181,7 +181,8 @@ void LazyCDProof::addLazyStep(Node expected,
     }
     Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
                           << " set (trusted) step " << idNull << "\n";
-    addStep(expected, idNull, {}, {expected});
+    Node tid = mkTrustId(idNull);
+    addStep(expected, ProofRule::TRUST, {}, {tid, expected});
     return;
   }
   Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected
diff --git a/src/proof/lazy_proof.h b/src/proof/lazy_proof.h
index 637b2129bba..e606169c735 100644
--- a/src/proof/lazy_proof.h
+++ b/src/proof/lazy_proof.h
@@ -20,6 +20,7 @@
 
 #include "context/cdhashset.h"
 #include "proof/proof.h"
+#include "proof/trust_id.h"
 
 namespace cvc5::internal {
 
@@ -90,7 +91,7 @@ class LazyCDProof : public CDProof
    */
   void addLazyStep(Node expected,
                    ProofGenerator* pg,
-                   ProofRule trustId = ProofRule::ASSUME,
+                   TrustId trustId = TrustId::NONE,
                    bool isClosed = false,
                    const char* ctx = "LazyCDProof::addLazyStep",
                    bool forceOverwrite = false);
diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp
index 22e93a46a7f..1d2137bc9c4 100644
--- a/src/proof/proof.cpp
+++ b/src/proof/proof.cpp
@@ -257,6 +257,21 @@ void CDProof::notifyNewProof(Node expected)
   }
 }
 
+bool CDProof::addTrustedStep(Node expected,
+                             TrustId id,
+                             const std::vector<Node>& children,
+                             const std::vector<Node>& args,
+                             bool ensureChildren,
+                             CDPOverwrite opolicy)
+{
+  std::vector<Node> sargs;
+  sargs.push_back(mkTrustId(id));
+  sargs.push_back(expected);
+  sargs.insert(sargs.end(), args.begin(), args.end());
+  return addStep(
+      expected, ProofRule::TRUST, children, sargs, ensureChildren, opolicy);
+}
+
 bool CDProof::addStep(Node expected,
                       const ProofStep& step,
                       bool ensureChildren,
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 1b50d50adba..55c87eb93ab 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "proof/proof_generator.h"
 #include "proof/proof_step_buffer.h"
+#include "proof/trust_id.h"
 #include "smt/env_obj.h"
 
 namespace cvc5::internal {
@@ -198,6 +199,17 @@ class CDProof : protected EnvObj, public ProofGenerator
                const std::vector<Node>& args,
                bool ensureChildren = false,
                CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY);
+  /**
+   * Version with trusted id. The arguments are optional additional arguments
+   * to the required arguments of ProofRule::TRUST. If none are provided, the
+   * trust id and the conclusion will be the arguments of the step.
+   */
+  bool addTrustedStep(Node expected,
+                      TrustId id,
+                      const std::vector<Node>& children,
+                      const std::vector<Node>& args,
+                      bool ensureChildren = false,
+                      CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY);
   /** Version with ProofStep */
   bool addStep(Node expected,
                const ProofStep& step,
diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index 34f38644b35..7e1f2268970 100644
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -61,6 +61,19 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
   return pn;
 }
 
+std::shared_ptr<ProofNode> ProofNodeManager::mkTrustedNode(
+    TrustId id,
+    const std::vector<std::shared_ptr<ProofNode>>& children,
+    const std::vector<Node>& args,
+    const Node& conc)
+{
+  std::vector<Node> sargs;
+  sargs.push_back(mkTrustId(id));
+  sargs.push_back(conc);
+  sargs.insert(sargs.end(), args.begin(), args.end());
+  return mkNode(ProofRule::TRUST, children, sargs);
+}
+
 std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
 {
   Assert(!fact.isNull());
diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h
index 8f74d03a982..b0a08dd912d 100644
--- a/src/proof/proof_node_manager.h
+++ b/src/proof/proof_node_manager.h
@@ -20,8 +20,9 @@
 
 #include <vector>
 
-#include "expr/node.h"
 #include "cvc5/cvc5_proof_rule.h"
+#include "expr/node.h"
+#include "proof/trust_id.h"
 
 namespace cvc5::internal {
 
@@ -84,6 +85,27 @@ class ProofNodeManager
       const std::vector<std::shared_ptr<ProofNode>>& children,
       const std::vector<Node>& args,
       Node expected = Node::null());
+  /**
+   * This constructs a ProofNode with rule ProofRule::TRUST with the given
+   * children and arguments.
+   *
+   * @param id The id of the proof node.
+   * @param children The children of the proof node.
+   * @param args The arguments of the proof node, which are optional additional
+   * arguments of ProofRule::TRUST beyond id and conc.
+   * @param conc The conclusion of the proof node.
+   * @param expected The conclusion of the proof node.
+   * @return the proof node, or nullptr if the given arguments do not
+   * consistute a proof of the expected conclusion according to the underlying
+   * checker, if both are provided. It also returns nullptr if neither the
+   * checker nor the expected field is provided, since in this case the
+   * conclusion is unknown.
+   */
+  std::shared_ptr<ProofNode> mkTrustedNode(
+      TrustId id,
+      const std::vector<std::shared_ptr<ProofNode>>& children,
+      const std::vector<Node>& args,
+      const Node& conc);
   /**
    * Make the proof node corresponding to the assumption of fact.
    *
diff --git a/src/proof/proof_node_to_sexpr.cpp b/src/proof/proof_node_to_sexpr.cpp
index 8ffa75c542e..54aeb7ced79 100644
--- a/src/proof/proof_node_to_sexpr.cpp
+++ b/src/proof/proof_node_to_sexpr.cpp
@@ -194,6 +194,27 @@ Node ProofNodeToSExpr::getOrMkMethodIdVariable(TNode n)
   d_midMap[mid] = var;
   return var;
 }
+Node ProofNodeToSExpr::getOrMkTrustIdVariable(TNode n)
+{
+  TrustId tid;
+  if (!getTrustId(n, tid))
+  {
+    // just use self if we failed to get the node, throw a debug failure
+    Assert(false) << "Expected trust id node, got " << n;
+    return n;
+  }
+  std::map<TrustId, Node>::iterator it = d_tridMap.find(tid);
+  if (it != d_tridMap.end())
+  {
+    return it->second;
+  }
+  std::stringstream ss;
+  ss << tid;
+  NodeManager* nm = NodeManager::currentNM();
+  Node var = nm->mkBoundVar(ss.str(), nm->sExprType());
+  d_tridMap[tid] = var;
+  return var;
+}
 Node ProofNodeToSExpr::getOrMkInferenceIdVariable(TNode n)
 {
   theory::InferenceId iid;
@@ -260,6 +281,7 @@ Node ProofNodeToSExpr::getArgument(Node arg, ArgFormat f)
     case ArgFormat::KIND: return getOrMkKindVariable(arg);
     case ArgFormat::THEORY_ID: return getOrMkTheoryIdVariable(arg);
     case ArgFormat::METHOD_ID: return getOrMkMethodIdVariable(arg);
+    case ArgFormat::TRUST_ID: return getOrMkTrustIdVariable(arg);
     case ArgFormat::INFERENCE_ID: return getOrMkInferenceIdVariable(arg);
     case ArgFormat::DSL_REWRITE_ID: return getOrMkDslRewriteVariable(arg);
     case ArgFormat::NODE_VAR: return getOrMkNodeVariable(arg);
@@ -289,7 +311,7 @@ ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
     }
     break;
     case ProofRule::SUBS:
-    case ProofRule::REWRITE:
+    case ProofRule::MACRO_REWRITE:
     case ProofRule::MACRO_SR_EQ_INTRO:
     case ProofRule::MACRO_SR_PRED_INTRO:
     case ProofRule::MACRO_SR_PRED_TRANSFORM:
@@ -299,13 +321,12 @@ ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
       }
       break;
     case ProofRule::MACRO_SR_PRED_ELIM: return ArgFormat::METHOD_ID; break;
-    case ProofRule::THEORY_LEMMA:
-    case ProofRule::THEORY_REWRITE:
+    case ProofRule::TRUST_THEORY_REWRITE:
       if (i == 1)
       {
         return ArgFormat::THEORY_ID;
       }
-      else if (r == ProofRule::THEORY_REWRITE && i == 2)
+      else if (i == 2)
       {
         return ArgFormat::METHOD_ID;
       }
@@ -333,6 +354,23 @@ ProofNodeToSExpr::ArgFormat ProofNodeToSExpr::getArgumentFormat(
         return ArgFormat::INFERENCE_ID;
       }
       break;
+    case ProofRule::TRUST:
+    {
+      if (i == 0)
+      {
+        return ArgFormat::TRUST_ID;
+      }
+      else if (i == 2)
+      {
+        TrustId tid;
+        getTrustId(pn->getArguments()[0], tid);
+        if (tid == TrustId::THEORY_LEMMA || tid == TrustId::THEORY_INFERENCE)
+        {
+          return ArgFormat::THEORY_ID;
+        }
+      }
+    }
+    break;
     default: break;
   }
   return ArgFormat::DEFAULT;
diff --git a/src/proof/proof_node_to_sexpr.h b/src/proof/proof_node_to_sexpr.h
index 514791f7a57..b74a9bd0084 100644
--- a/src/proof/proof_node_to_sexpr.h
+++ b/src/proof/proof_node_to_sexpr.h
@@ -20,10 +20,11 @@
 
 #include <map>
 
+#include "cvc5/cvc5_proof_rule.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "proof/method_id.h"
-#include "cvc5/cvc5_proof_rule.h"
+#include "proof/trust_id.h"
 #include "rewriter/rewrites.h"
 #include "theory/inference_id.h"
 #include "theory/theory_id.h"
@@ -64,6 +65,8 @@ class ProofNodeToSExpr
     THEORY_ID,
     // print the argument as a method id
     METHOD_ID,
+    // print the arugment as a trust id
+    TRUST_ID,
     // print the argument as an inference id
     INFERENCE_ID,
     // print the argument as a DSL rewrite id
@@ -85,6 +88,8 @@ class ProofNodeToSExpr
   std::map<theory::TheoryId, Node> d_tidMap;
   /** map method ids to a variable displaying the method id they represent */
   std::map<MethodId, Node> d_midMap;
+  /** map trust ids to a variable displaying the method id they represent */
+  std::map<TrustId, Node> d_tridMap;
   /** map infer ids to a variable displaying the inference id they represent */
   std::map<theory::InferenceId, Node> d_iidMap;
   /** map dsl rewrite ids to a variable displaying the dsl rewrite id they
@@ -109,6 +114,8 @@ class ProofNodeToSExpr
   Node getOrMkTheoryIdVariable(TNode n);
   /** get or make method id variable */
   Node getOrMkMethodIdVariable(TNode n);
+  /** get or make trust id variable */
+  Node getOrMkTrustIdVariable(TNode n);
   /** get or make inference id variable */
   Node getOrMkInferenceIdVariable(TNode n);
   /** get or make DSL rewrite id variable */
diff --git a/src/proof/proof_step_buffer.cpp b/src/proof/proof_step_buffer.cpp
index 1b1f693856a..7d89c46f531 100644
--- a/src/proof/proof_step_buffer.cpp
+++ b/src/proof/proof_step_buffer.cpp
@@ -120,6 +120,17 @@ bool ProofStepBuffer::addStep(ProofRule id,
       std::pair<Node, ProofStep>(expected, ProofStep(id, children, args)));
   return true;
 }
+bool ProofStepBuffer::addTrustedStep(TrustId id,
+                                     const std::vector<Node>& children,
+                                     const std::vector<Node>& args,
+                                     Node conc)
+{
+  std::vector<Node> sargs;
+  sargs.push_back(mkTrustId(id));
+  sargs.push_back(conc);
+  sargs.insert(sargs.end(), args.begin(), args.end());
+  return addStep(ProofRule::TRUST, children, sargs, conc);
+}
 
 void ProofStepBuffer::addSteps(ProofStepBuffer& psb)
 {
diff --git a/src/proof/proof_step_buffer.h b/src/proof/proof_step_buffer.h
index 0d23b518473..b6dd40d5e47 100644
--- a/src/proof/proof_step_buffer.h
+++ b/src/proof/proof_step_buffer.h
@@ -20,8 +20,9 @@
 
 #include <vector>
 
-#include "expr/node.h"
 #include "cvc5/cvc5_proof_rule.h"
+#include "expr/node.h"
+#include "proof/trust_id.h"
 
 namespace cvc5::internal {
 
@@ -99,6 +100,11 @@ class ProofStepBuffer
                const std::vector<Node>& children,
                const std::vector<Node>& args,
                Node expected);
+  /** Add trusted step */
+  bool addTrustedStep(TrustId id,
+                      const std::vector<Node>& children,
+                      const std::vector<Node>& args,
+                      Node conc);
   /** Multi-step version */
   void addSteps(ProofStepBuffer& psb);
   /** pop step */
diff --git a/src/proof/trust_id.cpp b/src/proof/trust_id.cpp
new file mode 100644
index 00000000000..c0d908c35be
--- /dev/null
+++ b/src/proof/trust_id.cpp
@@ -0,0 +1,71 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2023 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of trust identifier
+ */
+
+#include "proof/trust_id.h"
+
+#include "proof/proof_checker.h"
+#include "util/rational.h"
+
+using namespace cvc5::internal::kind;
+
+namespace cvc5::internal {
+
+const char* toString(TrustId id)
+{
+  switch (id)
+  {
+    case TrustId::NONE: return "NONE";
+    case TrustId::THEORY_LEMMA: return "THEORY_LEMMA";
+    case TrustId::THEORY_INFERENCE: return "THEORY_INFERENCE";
+    case TrustId::PREPROCESS: return "PREPROCESS";
+    case TrustId::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
+    case TrustId::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
+    case TrustId::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
+    case TrustId::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF";
+    case TrustId::WITNESS_AXIOM: return "WITNESS_AXIOM";
+    case TrustId::REWRITE_NO_ELABORATE: return "REWRITE_NO_ELABORATE";
+    case TrustId::FLATTENING_REWRITE: return "FLATTENING_REWRITE";
+    case TrustId::SUBS_NO_ELABORATE: return "SUBS_NO_ELABORATE";
+    case TrustId::SUBS_MAP: return "SUBS_MAP";
+    case TrustId::SUBS_EQ: return "SUBS_EQ";
+    case TrustId::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS";
+    default: return "TrustId::Unknown";
+  };
+}
+
+std::ostream& operator<<(std::ostream& out, TrustId id)
+{
+  out << toString(id);
+  return out;
+}
+
+Node mkTrustId(TrustId id)
+{
+  return NodeManager::currentNM()->mkConstInt(
+      Rational(static_cast<uint32_t>(id)));
+}
+
+bool getTrustId(TNode n, TrustId& i)
+{
+  uint32_t index;
+  if (!ProofRuleChecker::getUInt32(n, index))
+  {
+    return false;
+  }
+  i = static_cast<TrustId>(index);
+  return true;
+}
+
+}  // namespace cvc5::internal
diff --git a/src/proof/trust_id.h b/src/proof/trust_id.h
new file mode 100644
index 00000000000..be3ba869c1b
--- /dev/null
+++ b/src/proof/trust_id.h
@@ -0,0 +1,73 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2023 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Trust identifier enumeration
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__TRUST_ID_H
+#define CVC5__PROOF__TRUST_ID_H
+
+#include "expr/node.h"
+
+namespace cvc5::internal {
+
+/**
+ * Identifiers for trusted steps in proofs.
+ */
+enum class TrustId : uint32_t
+{
+  NONE,
+  /** A lemma sent by a theory without a proof */
+  THEORY_LEMMA,
+  /** An internal inference made by a theory without a proof */
+  THEORY_INFERENCE,
+  /** A rewrite of the input formula by a preprocessing pass without a proof */
+  PREPROCESS,
+  /** A lemma added during preprocessing without a proof */
+  PREPROCESS_LEMMA,
+  /** A rewrite of the input formula made by a theory during preprocessing
+     without a proof */
+  THEORY_PREPROCESS,
+  /** A lemma added during theory-preprocessing without a proof */
+  THEORY_PREPROCESS_LEMMA,
+  /** A expanding of definitions of the input formula made without a proof */
+  THEORY_EXPAND_DEF,
+  /** An axiom for an introduced witness term without a corresponding proof */
+  WITNESS_AXIOM,
+  /** A rewrite whose proof could not be elaborated */
+  REWRITE_NO_ELABORATE,
+  /** A flattening rewrite in an equality engine proof */
+  FLATTENING_REWRITE,
+  /** A proof of an applied substitution that could not be no elaborate */
+  SUBS_NO_ELABORATE,
+  /** A proof of an applied substitution that could not be reconstructed during
+     solving */
+  SUBS_MAP,
+  /** A proof of a substitution x=t that could not be shown by rewrite */
+  SUBS_EQ,
+  /** A quantifiers preprocessing step that was given without a proof */
+  QUANTIFIERS_PREPROCESS,
+};
+/** Converts a trust id to a string. */
+const char* toString(TrustId id);
+/** Write a trust id to out */
+std::ostream& operator<<(std::ostream& out, TrustId id);
+/** Make a trust id node */
+Node mkTrustId(TrustId id);
+/** get a trust identifier from a node, return false if we fail */
+bool getTrustId(TNode n, TrustId& i);
+
+}  // namespace cvc5::internal
+
+#endif /* CVC5__PROOF__METHOD_ID_H */
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 39e1708dae1..9b6fb6feed5 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -159,7 +159,7 @@ void ProofCnfStream::convertAndAssert(TNode node,
     Node toJustify = negated ? node.notNode() : static_cast<Node>(node);
     d_proof.addLazyStep(toJustify,
                         pg,
-                        ProofRule::ASSUME,
+                        TrustId::NONE,
                         true,
                         "ProofCnfStream::convertAndAssert:cnf");
   }
@@ -633,7 +633,7 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
                        << trn.identifyGenerator() << std::endl;
     d_proof.addLazyStep(proven,
                         trn.getGenerator(),
-                        ProofRule::ASSUME,
+                        TrustId::NONE,
                         true,
                         "ProofCnfStream::convertPropagation");
   }
@@ -693,10 +693,8 @@ void ProofCnfStream::convertPropagation(TrustNode trn)
   }
   else
   {
-    d_proof.addStep(d_currPropagationProcessed,
-                    ProofRule::THEORY_LEMMA,
-                    {},
-                    {d_currPropagationProcessed});
+    d_proof.addTrustedStep(
+        d_currPropagationProcessed, TrustId::THEORY_LEMMA, {}, {});
   }
 }
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b023515084c..09ca6da432e 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -250,8 +250,7 @@ void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
       && !trn.getGenerator())
   {
     Node actualNode = negated ? node.notNode() : node;
-    d_theoryLemmaPg.addStep(
-        actualNode, ProofRule::THEORY_LEMMA, {}, {actualNode});
+    d_theoryLemmaPg.addTrustedStep(actualNode, TrustId::THEORY_LEMMA, {}, {});
     trn = TrustNode::mkReplaceGenTrustNode(trn, &d_theoryLemmaPg);
   }
   assertInternal(node, negated, removable, false, trn.getGenerator());
diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index c862e8617bc..3e9ee7553bc 100644
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -30,11 +30,8 @@
 namespace cvc5::internal {
 namespace smt {
 
-PreprocessProofGenerator::PreprocessProofGenerator(Env& env,
-                                                   context::Context* c,
-                                                   std::string name,
-                                                   ProofRule ra,
-                                                   ProofRule rpp)
+PreprocessProofGenerator::PreprocessProofGenerator(
+    Env& env, context::Context* c, std::string name, TrustId ra, TrustId rpp)
     : EnvObj(env),
       d_ctx(c ? c : &d_context),
       d_src(d_ctx),
@@ -186,7 +183,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
           {
             Node idr = mkMethodId(MethodId::RW_EXT_REWRITE);
             Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl;
-            cdp.addStep(proven, ProofRule::REWRITE, {}, {proven[0], idr});
+            cdp.addStep(proven, ProofRule::MACRO_REWRITE, {}, {proven[0], idr});
             proofStepProcessed = true;
           }
         }
@@ -210,8 +207,8 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
             << "...justify missing step with "
             << (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl;
         // add trusted step, the rule depends on the kind of trust node
-        cdp.addStep(
-            proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
+        Node tid = mkTrustId(tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp);
+        cdp.addStep(proven, ProofRule::TRUST, {}, {tid, proven});
       }
     }
   } while (success);
@@ -252,19 +249,19 @@ LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
 
 std::string PreprocessProofGenerator::identify() const { return d_name; }
 
-void PreprocessProofGenerator::checkEagerPedantic(ProofRule r)
+void PreprocessProofGenerator::checkEagerPedantic(TrustId r)
 {
   if (options().proof.proofCheck == options::ProofCheckMode::EAGER)
   {
     // catch a pedantic failure now, which otherwise would not be
     // triggered since we are doing lazy proof generation
     ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
-    if (pc->isPedanticFailure(r, nullptr))
+    if (pc->isPedanticFailure(ProofRule::TRUST, nullptr))
     {
       std::stringstream serr;
-      pc->isPedanticFailure(r, &serr);
-      Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
-                  << serr.str();
+      pc->isPedanticFailure(ProofRule::TRUST, &serr);
+      Unhandled() << "PreprocessProofGenerator::checkEagerPedantic (" << r
+                  << "): " << serr.str();
     }
   }
 }
diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index a1a0dfacaf6..aed39e3632d 100644
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -23,6 +23,7 @@
 #include "proof/proof.h"
 #include "proof/proof_generator.h"
 #include "proof/proof_set.h"
+#include "proof/trust_id.h"
 #include "proof/trust_node.h"
 #include "smt/env_obj.h"
 
@@ -63,16 +64,16 @@ class PreprocessProofGenerator : protected EnvObj, public ProofGenerator
    * @param env Reference to the environment
    * @param c The context this class depends on
    * @param name The name of this generator (for debugging)
-   * @param ra The proof rule to use when no generator is provided for new
+   * @param ra The id to use when no generator is provided for new
    * assertions
-   * @param rpp The proof rule to use when no generator is provided for
+   * @param rpp The id to use when no generator is provided for
    * preprocessing steps.
    */
   PreprocessProofGenerator(Env& env,
                            context::Context* c = nullptr,
                            std::string name = "PreprocessProofGenerator",
-                           ProofRule ra = ProofRule::PREPROCESS_LEMMA,
-                           ProofRule rpp = ProofRule::PREPROCESS);
+                           TrustId ra = TrustId::PREPROCESS_LEMMA,
+                           TrustId rpp = TrustId::PREPROCESS);
   ~PreprocessProofGenerator() {}
   /**
    * Notify that n is an input (its proof is ASSUME).
@@ -112,7 +113,7 @@ class PreprocessProofGenerator : protected EnvObj, public ProofGenerator
    * Possibly check pedantic failure for null proof generator provided
    * to this class.
    */
-  void checkEagerPedantic(ProofRule r);
+  void checkEagerPedantic(TrustId r);
   /** A dummy context used by this class if none is provided */
   context::Context d_context;
   /** The context used here */
@@ -135,9 +136,9 @@ class PreprocessProofGenerator : protected EnvObj, public ProofGenerator
   /** Name for debugging */
   std::string d_name;
   /** The trust rule for new assertions with no provided proof generator */
-  ProofRule d_ra;
+  TrustId d_ra;
   /** The trust rule for rewrites with no provided proof generator */
-  ProofRule d_rpp;
+  TrustId d_rpp;
 };
 
 }  // namespace smt
diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
index 8016b2e6c56..eb0e1957e88 100644
--- a/src/smt/proof_final_callback.cpp
+++ b/src/smt/proof_final_callback.cpp
@@ -45,6 +45,8 @@ ProofFinalCallback::ProofFinalCallback(Env& env)
       d_dslRuleCount(
           statisticsRegistry().registerHistogram<rewriter::DslProofRule>(
               "finalProof::dslRuleCount")),
+      d_trustIds(statisticsRegistry().registerHistogram<TrustId>(
+          "finalProof::trustCount")),
       d_totalRuleCount(
           statisticsRegistry().registerInt("finalProof::totalRuleCount")),
       d_minPedanticLevel(
@@ -137,11 +139,22 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
       }
     }
   }
+  else if (r == ProofRule::TRUST)
+  {
+    TrustId id;
+    Trace("final-pf-hole") << "hole TRUST";
+    if (getTrustId(pn->getArguments()[0], id))
+    {
+      d_trustIds << id;
+      Trace("final-pf-hole") << " " << id;
+    }
+    Trace("final-pf-hole") << ": " << pn->getResult() << std::endl;
+  }
   // print for debugging
   if (TraceIsOn("final-pf-hole"))
   {
     // currently only track theory rewrites
-    if (r == ProofRule::THEORY_REWRITE)
+    if (r == ProofRule::TRUST_THEORY_REWRITE)
     {
       const std::vector<Node>& args = pn->getArguments();
       Node eq = args[0];
@@ -150,7 +163,7 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
       Trace("final-pf-hole") << "hole " << r << " " << tid << " : " << eq[0]
                              << " ---> " << eq[1] << std::endl;
     }
-    else if (r == ProofRule::REWRITE)
+    else if (r == ProofRule::MACRO_REWRITE)
     {
       const std::vector<Node>& args = pn->getArguments();
       Node eq = args[0];
diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h
index ea5e4143380..8ce33acc0d5 100644
--- a/src/smt/proof_final_callback.h
+++ b/src/smt/proof_final_callback.h
@@ -23,6 +23,7 @@
 #include <unordered_set>
 
 #include "proof/proof_node_updater.h"
+#include "proof/trust_id.h"
 #include "rewriter/rewrites.h"
 #include "smt/env_obj.h"
 #include "theory/inference_id.h"
@@ -61,9 +62,14 @@ class ProofFinalCallback : protected EnvObj, public ProofNodeUpdaterCallback
    * marked with the given inference id.
    */
   HistogramStat<theory::InferenceId> d_annotationRuleIds;
-  /** Counts number of postprocessed proof nodes for each kind of DSL proof rule
+  /**
+   * Counts number of postprocessed proof nodes for each kind of DSL proof rule
    */
   HistogramStat<rewriter::DslProofRule> d_dslRuleCount;
+  /**
+   * Counts number of postprocessed proof nodes for each trusted step
+   */
+  HistogramStat<TrustId> d_trustIds;
   /** Total number of postprocessed rule applications */
   IntStat d_totalRuleCount;
   /** The minimum pedantic level of any rule encountered */
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index b353bebdfa9..8de138664a7 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -89,7 +89,7 @@ PfManager::PfManager(Env& env)
         != options::ProofGranularityMode::REWRITE)
     {
       d_pfpp->setEliminateRule(ProofRule::SUBS);
-      d_pfpp->setEliminateRule(ProofRule::REWRITE);
+      d_pfpp->setEliminateRule(ProofRule::MACRO_REWRITE);
       if (options().proof.proofGranularityMode
           != options::ProofGranularityMode::THEORY_REWRITE)
       {
@@ -98,8 +98,8 @@ PfManager::PfManager(Env& env)
       }
     }
     // theory-specific lazy proof reconstruction
-    d_pfpp->setEliminateRule(ProofRule::STRING_INFERENCE);
-    d_pfpp->setEliminateRule(ProofRule::BV_BITBLAST);
+    d_pfpp->setEliminateRule(ProofRule::MACRO_STRING_INFERENCE);
+    d_pfpp->setEliminateRule(ProofRule::MACRO_BV_BITBLAST);
   }
   d_false = NodeManager::currentNM()->mkConst(false);
 }
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 19416a2253b..140600134a7 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -262,10 +262,10 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
     {
       Node eq = ts.eqNode(tr);
       // apply REWRITE proof rule
-      if (!updateInternal(eq, ProofRule::REWRITE, {}, rargs, cdp))
+      if (!updateInternal(eq, ProofRule::MACRO_REWRITE, {}, rargs, cdp))
       {
         // if not elimianted, add as step
-        cdp->addStep(eq, ProofRule::REWRITE, {}, rargs);
+        cdp->addStep(eq, ProofRule::MACRO_REWRITE, {}, rargs);
       }
       tchildren.push_back(eq);
     }
@@ -782,7 +782,7 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
             << eq << std::endl
             << eqq << std::endl
             << "from " << children << " applied to " << t << std::endl;
-        cdp->addStep(eqq, ProofRule::TRUST_SUBS, children, {eqq});
+        cdp->addTrustedStep(eqq, TrustId::SUBS_NO_ELABORATE, children, {});
       }
     }
     else
@@ -791,7 +791,7 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
     }
     return eqq;
   }
-  else if (id == ProofRule::REWRITE)
+  else if (id == ProofRule::MACRO_REWRITE)
   {
     // get the kind of rewrite
     MethodId idr = MethodId::RW_REWRITE;
@@ -817,15 +817,16 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
         // did not have a proof of rewriting, probably isExtEq is true
         if (isExtEq)
         {
-          // update to THEORY_REWRITE with idr
+          // update to TRUST_THEORY_REWRITE with idr
           Assert(args.size() >= 1);
           Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
-          cdp->addStep(eq, ProofRule::THEORY_REWRITE, {}, {eq, tid, args[1]});
+          cdp->addStep(
+              eq, ProofRule::TRUST_THEORY_REWRITE, {}, {eq, tid, args[1]});
         }
         else
         {
           // this should never be applied
-          cdp->addStep(eq, ProofRule::TRUST_REWRITE, {}, {eq});
+          cdp->addTrustedStep(eq, TrustId::REWRITE_NO_ELABORATE, {}, {});
         }
       }
       else
@@ -863,7 +864,7 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
           // will expand this as a default rewrite if needed
           Node eqd = retCurr.eqNode(retDef);
           Node mid = mkMethodId(midi);
-          cdp->addStep(eqd, ProofRule::REWRITE, {}, {retCurr, mid});
+          cdp->addStep(eqd, ProofRule::MACRO_REWRITE, {}, {retCurr, mid});
           transEq.push_back(eqd);
         }
         retCurr = retDef;
@@ -885,7 +886,8 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
         // in this case, must be a non-standard rewrite kind
         Assert(args.size() >= 2);
         targs.push_back(args[1]);
-        Node eqpp = expandMacros(ProofRule::THEORY_REWRITE, {}, targs, cdp);
+        Node eqpp =
+            expandMacros(ProofRule::TRUST_THEORY_REWRITE, {}, targs, cdp);
         transEq.push_back(eqp);
         if (eqpp.isNull())
         {
@@ -959,7 +961,7 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
                           << std::endl;
     return sumBounds;
   }
-  else if (id == ProofRule::STRING_INFERENCE)
+  else if (id == ProofRule::MACRO_STRING_INFERENCE)
   {
     // get the arguments
     Node conc;
@@ -976,7 +978,7 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
       }
     }
   }
-  else if (id == ProofRule::BV_BITBLAST)
+  else if (id == ProofRule::MACRO_BV_BITBLAST)
   {
     bv::BBProof bb(d_env, nullptr, true);
     Node eq = args[0];
@@ -1003,7 +1005,7 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
     TheoryId tid = THEORY_LAST;
     MethodId mid = MethodId::RW_REWRITE;
     // if theory rewrite, get diagnostic information
-    if (id == ProofRule::THEORY_REWRITE)
+    if (id == ProofRule::TRUST_THEORY_REWRITE)
     {
       builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid);
       getMethodId(args[2], mid);
@@ -1024,9 +1026,6 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
     }
     // otherwise no update
   }
-
-  // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
-
   return Node::null();
 }
 
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 321e310c7fb..b8bf399f628 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -378,7 +378,7 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node,
           ProofGenerator* expg = sm->getProofGenerator(existsAssertion);
           d_lp->addLazyStep(existsAssertion,
                             expg,
-                            ProofRule::WITNESS_AXIOM,
+                            TrustId::WITNESS_AXIOM,
                             true,
                             "RemoveTermFormulas::run:skolem_pf");
           d_lp->addStep(
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 6b05965b00e..9fc9ac10363 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -95,7 +95,7 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
           // k = t
           d_wintroPf.addStep(eq, ProofRule::SKOLEM_INTRO, {}, {cur});
           d_tcpg.addRewriteStep(
-              cur, curw, &d_wintroPf, true, ProofRule::ASSUME, true);
+              cur, curw, &d_wintroPf, true, TrustId::NONE, true);
           // recursively transform
           visit.push_back(curw);
         }
diff --git a/src/theory/arith/linear/constraint.cpp b/src/theory/arith/linear/constraint.cpp
index f14c25c1b8f..edba04ada72 100644
--- a/src/theory/arith/linear/constraint.cpp
+++ b/src/theory/arith/linear/constraint.cpp
@@ -1841,10 +1841,10 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
         {
           Node t =
               builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH);
-          pf = pnm->mkNode(ProofRule::THEORY_INFERENCE,
-                           children,
-                           {getProofLiteral(), t},
-                           getProofLiteral());
+          pf = pnm->mkTrustedNode(TrustId::THEORY_INFERENCE,
+                                  children,
+                                  {getProofLiteral(), t},
+                                  getProofLiteral());
           break;
         }
         case ArithProofType::TrichotomyAP:
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 13d67bfa752..9bea4d06d5c 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -493,7 +493,8 @@ SkolemLemma OperatorElim::mkSkolemLemma(Node lem, Node k)
   TrustNode tlem;
   if (d_env.isTheoryProofProducing())
   {
-    tlem = mkTrustNode(lem, ProofRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
+    Node tid = mkTrustId(TrustId::THEORY_PREPROCESS_LEMMA);
+    tlem = mkTrustNode(lem, ProofRule::TRUST, {}, {tid, lem});
   }
   else
   {
diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp
index 7345464e298..1525f29a03c 100644
--- a/src/theory/arith/pp_rewrite_eq.cpp
+++ b/src/theory/arith/pp_rewrite_eq.cpp
@@ -46,11 +46,12 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom)
   if (d_env.isTheoryProofProducing())
   {
     Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH);
+    Node eq = atom.eqNode(rewritten);
     return d_ppPfGen.mkTrustedRewrite(
         atom,
         rewritten,
-        d_env.getProofNodeManager()->mkNode(
-            ProofRule::THEORY_INFERENCE, {}, {atom.eqNode(rewritten), t}));
+        d_env.getProofNodeManager()->mkTrustedNode(
+            TrustId::THEORY_INFERENCE, {}, {}, eq));
   }
   return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
 }
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index 0e9e0da6c2c..049fe55b5ee 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -16,6 +16,7 @@
 #include "theory/arrays/inference_manager.h"
 
 #include "options/smt_options.h"
+#include "proof/trust_id.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/theory.h"
 #include "theory/theory_state.h"
@@ -114,15 +115,16 @@ void InferenceManager::convert(ProofRule& id,
       break;
     case ProofRule::ARRAYS_EXT: children.push_back(exp); break;
     default:
-      if (id != ProofRule::THEORY_INFERENCE)
+      if (id != ProofRule::TRUST)
       {
         Assert(false) << "Unknown rule " << id << "\n";
       }
       children.push_back(exp);
+      args.push_back(mkTrustId(TrustId::THEORY_INFERENCE));
       args.push_back(conc);
       args.push_back(
           builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARRAYS));
-      id = ProofRule::THEORY_INFERENCE;
+      id = ProofRule::TRUST;
       break;
   }
 }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 2d1d47818e8..8c9db3cc9fd 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1676,12 +1676,12 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     {
       preRegisterTermInternal(selConst);
     }
-    // not currently supported in proofs, use THEORY_INFERENCE
+    // not currently supported in proofs, use TRUST
     d_im.assertInference(selConst.eqNode(defValue),
                          true,
                          InferenceId::ARRAYS_CONST_ARRAY_DEFAULT,
                          d_true,
-                         ProofRule::THEORY_INFERENCE);
+                         ProofRule::TRUST);
   }
 
   const CTNodeList* stores = d_infoMap.getStores(a);
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 0f32e08c6ad..e144b6025c7 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -50,26 +50,14 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::ENCODE_PRED_TRANSFORM, this);
   pc->registerChecker(ProofRule::DSL_REWRITE, this);
   // rules depending on the rewriter
-  pc->registerTrustedChecker(ProofRule::REWRITE, this, 4);
+  pc->registerTrustedChecker(ProofRule::MACRO_REWRITE, this, 4);
   pc->registerTrustedChecker(ProofRule::MACRO_SR_EQ_INTRO, this, 4);
   pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_INTRO, this, 4);
   pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_ELIM, this, 4);
   pc->registerTrustedChecker(ProofRule::MACRO_SR_PRED_TRANSFORM, this, 4);
-  pc->registerTrustedChecker(ProofRule::THEORY_REWRITE, this, 4);
+  pc->registerTrustedChecker(ProofRule::TRUST_THEORY_REWRITE, this, 4);
   // trusted rules
-  pc->registerTrustedChecker(ProofRule::THEORY_LEMMA, this, 1);
-  pc->registerTrustedChecker(ProofRule::PREPROCESS, this, 3);
-  pc->registerTrustedChecker(ProofRule::PREPROCESS_LEMMA, this, 3);
-  pc->registerTrustedChecker(ProofRule::THEORY_PREPROCESS, this, 3);
-  pc->registerTrustedChecker(ProofRule::THEORY_PREPROCESS_LEMMA, this, 3);
-  pc->registerTrustedChecker(ProofRule::THEORY_EXPAND_DEF, this, 3);
-  pc->registerTrustedChecker(ProofRule::WITNESS_AXIOM, this, 3);
-  pc->registerTrustedChecker(ProofRule::TRUST_REWRITE, this, 1);
-  pc->registerTrustedChecker(ProofRule::TRUST_FLATTENING_REWRITE, this, 1);
-  pc->registerTrustedChecker(ProofRule::TRUST_SUBS, this, 1);
-  pc->registerTrustedChecker(ProofRule::TRUST_SUBS_MAP, this, 1);
-  pc->registerTrustedChecker(ProofRule::TRUST_SUBS_EQ, this, 3);
-  pc->registerTrustedChecker(ProofRule::THEORY_INFERENCE, this, 3);
+  pc->registerTrustedChecker(ProofRule::TRUST, this, 1);
   // external proof rules
   pc->registerChecker(ProofRule::LFSC_RULE, this);
   pc->registerChecker(ProofRule::ALETHE_RULE, this);
@@ -264,7 +252,7 @@ Node BuiltinProofRuleChecker::checkInternal(ProofRule id,
     }
     return args[0].eqNode(res);
   }
-  else if (id == ProofRule::REWRITE)
+  else if (id == ProofRule::MACRO_REWRITE)
   {
     Assert(children.empty());
     Assert(1 <= args.size() && args.size() <= 2);
@@ -393,16 +381,12 @@ Node BuiltinProofRuleChecker::checkInternal(ProofRule id,
     Assert(args.size() == 1);
     return RemoveTermFormulas::getAxiomFor(args[0]);
   }
-  else if (id == ProofRule::PREPROCESS || id == ProofRule::PREPROCESS_LEMMA
-           || id == ProofRule::THEORY_PREPROCESS
-           || id == ProofRule::THEORY_PREPROCESS_LEMMA
-           || id == ProofRule::THEORY_EXPAND_DEF
-           || id == ProofRule::WITNESS_AXIOM || id == ProofRule::THEORY_LEMMA
-           || id == ProofRule::THEORY_REWRITE
-           || id == ProofRule::TRUST_FLATTENING_REWRITE
-           || id == ProofRule::TRUST_REWRITE || id == ProofRule::TRUST_SUBS
-           || id == ProofRule::TRUST_SUBS_MAP || id == ProofRule::TRUST_SUBS_EQ
-           || id == ProofRule::THEORY_INFERENCE)
+  else if (id == ProofRule::TRUST)
+  {
+    Assert(args.size() >= 2);
+    return args[1];
+  }
+  else if (id == ProofRule::TRUST_THEORY_REWRITE)
   {
     // "trusted" rules
     Assert(!args.empty());
diff --git a/src/theory/bv/bitblast/bitblast_proof_generator.cpp b/src/theory/bv/bitblast/bitblast_proof_generator.cpp
index 394cea2e3fd..027f4394897 100644
--- a/src/theory/bv/bitblast/bitblast_proof_generator.cpp
+++ b/src/theory/bv/bitblast/bitblast_proof_generator.cpp
@@ -35,7 +35,7 @@ std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
   /* Coarse-grained bit-blast step. */
   if (t.isNull())
   {
-    cdp.addStep(eq, ProofRule::BV_BITBLAST, {}, {eq});
+    cdp.addStep(eq, ProofRule::MACRO_BV_BITBLAST, {}, {eq});
   }
   else
   {
@@ -85,7 +85,7 @@ std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
     // Record pre-rewrite of bit-vector atom.
     if (t != rwt)
     {
-      cdp.addStep(t.eqNode(rwt), ProofRule::REWRITE, {}, {t});
+      cdp.addStep(t.eqNode(rwt), ProofRule::MACRO_REWRITE, {}, {t});
       transSteps.push_back(t.eqNode(rwt));
     }
 
@@ -97,7 +97,7 @@ std::shared_ptr<ProofNode> BitblastProofGenerator::getProofFor(Node eq)
     Node rwbbt = rewrite(bbt);
     if (bbt != rwbbt)
     {
-      cdp.addStep(bbt.eqNode(rwbbt), ProofRule::REWRITE, {}, {bbt});
+      cdp.addStep(bbt.eqNode(rwbbt), ProofRule::MACRO_REWRITE, {}, {bbt});
       transSteps.push_back(bbt.eqNode(rwbbt));
     }
 
diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp
index 60b2840c245..9fe80c0a4e4 100644
--- a/src/theory/bv/proof_checker.cpp
+++ b/src/theory/bv/proof_checker.cpp
@@ -21,8 +21,8 @@ namespace bv {
 
 void BVProofRuleChecker::registerTo(ProofChecker* pc)
 {
-  pc->registerChecker(ProofRule::BV_BITBLAST, this);
-  pc->registerChecker(ProofRule::BV_BITBLAST_STEP, this);
+  pc->registerTrustedChecker(ProofRule::MACRO_BV_BITBLAST, this, 2);
+  pc->registerTrustedChecker(ProofRule::BV_BITBLAST_STEP, this, 2);
   pc->registerChecker(ProofRule::BV_EAGER_ATOM, this);
 }
 
@@ -30,7 +30,7 @@ Node BVProofRuleChecker::checkInternal(ProofRule id,
                                        const std::vector<Node>& children,
                                        const std::vector<Node>& args)
 {
-  if (id == ProofRule::BV_BITBLAST)
+  if (id == ProofRule::MACRO_BV_BITBLAST)
   {
     Assert(children.empty());
     Assert(args.size() == 1);
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 02483437cf7..6448287cdf4 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -32,6 +32,7 @@ namespace datatypes {
 InferProofCons::InferProofCons(Env& env, context::Context* c)
     : EnvObj(env), d_lazyFactMap(c == nullptr ? &d_context : c)
 {
+  d_tdid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_DATATYPES);
 }
 
 void InferProofCons::notifyFact(const std::shared_ptr<DatatypesInference>& di)
@@ -277,8 +278,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
   {
     // failed to reconstruct, add trust
     Trace("dt-ipc") << "...failed " << infer << std::endl;
-    Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_DATATYPES);
-    cdp->addStep(conc, ProofRule::THEORY_INFERENCE, expv, {conc, t});
+    cdp->addTrustedStep(conc, TrustId::THEORY_INFERENCE, expv, {d_tdid});
   }
   else
   {
diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h
index adde69487e3..28acdda06ef 100644
--- a/src/theory/datatypes/infer_proof_cons.h
+++ b/src/theory/datatypes/infer_proof_cons.h
@@ -72,6 +72,8 @@ class InferProofCons : protected EnvObj, public ProofGenerator
   virtual std::string identify() const override;
 
  private:
+  /** Common constants */
+  Node d_tdid;
   /** convert
    *
    * This method is called when the theory of strings makes an inference
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index dca4282147d..75427c8ffff 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -287,7 +287,7 @@ bool Instantiate::addInstantiationInternal(
       // add the transformation proof, or the trusted rule if none provided
       pfTmp->addLazyStep(proven,
                          tpBody.getGenerator(),
-                         ProofRule::QUANTIFIERS_PREPROCESS,
+                         TrustId::QUANTIFIERS_PREPROCESS,
                          true,
                          "Instantiate::getInstantiation:qpreprocess");
       pfTmp->addStep(body, ProofRule::EQ_RESOLVE, {orig_body, proven}, {});
@@ -596,7 +596,7 @@ Node Instantiate::getInstantiation(Node q,
         Node proven = trn.getProven();
         pf->addLazyStep(proven,
                         trn.getGenerator(),
-                        ProofRule::THEORY_PREPROCESS,
+                        TrustId::THEORY_PREPROCESS,
                         true,
                         "Instantiate::getInstantiation:rewrite_inst");
         pf->addStep(newBody, ProofRule::EQ_RESOLVE, {body, proven}, {});
diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
index 352c48f2ecf..388388e8732 100644
--- a/src/theory/quantifiers/proof_checker.cpp
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -33,8 +33,6 @@ void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::SKOLEMIZE, this);
   pc->registerChecker(ProofRule::INSTANTIATE, this);
   pc->registerChecker(ProofRule::ALPHA_EQUIV, this);
-  // trusted rules
-  pc->registerTrustedChecker(ProofRule::QUANTIFIERS_PREPROCESS, this, 3);
 }
 
 Node QuantifiersProofRuleChecker::checkInternal(
@@ -134,12 +132,6 @@ Node QuantifiersProofRuleChecker::checkInternal(
         vars.begin(), vars.end(), newVars.begin(), newVars.end());
     return args[0].eqNode(renamedBody);
   }
-  else if (id == ProofRule::QUANTIFIERS_PREPROCESS)
-  {
-    Assert(!args.empty());
-    Assert(args[0].getType().isBoolean());
-    return args[0];
-  }
 
   // no rule
   return Node::null();
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 8ee4f84190e..4d71016faaa 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -375,11 +375,12 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
             Node eq = rewriteStackTop.d_node.eqNode(cached);
             // we make this a post-rewrite, since we are processing a node that
             // has finished post-rewriting above
+            Node trrid = mkTrustId(TrustId::REWRITE_NO_ELABORATE);
             tcpg->addRewriteStep(rewriteStackTop.d_node,
                                  cached,
-                                 ProofRule::TRUST_REWRITE,
+                                 ProofRule::TRUST,
                                  {},
-                                 {eq},
+                                 {trrid, eq},
                                  false);
             // don't overwrite the cache, should be the same
             rewriteStackTop.d_node = cached;
@@ -466,7 +467,7 @@ RewriteResponse Rewriter::processTrustRewriteResponse(
                                   : MethodId::RW_REWRITE_THEORY_POST);
       tcpg->addRewriteStep(proven[0],
                            proven[1],
-                           ProofRule::THEORY_REWRITE,
+                           ProofRule::TRUST_THEORY_REWRITE,
                            {},
                            {proven, tidn, rid},
                            isPre);
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 54be7d74fb7..2edcfeded51 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -24,7 +24,9 @@
 #include "options/quantifiers_options.h"
 #include "options/sep_options.h"
 #include "options/smt_options.h"
+#include "proof/trust_id.h"
 #include "smt/logic_exception.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
@@ -55,6 +57,8 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation)
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
+  d_tiid = mkTrustId(TrustId::THEORY_INFERENCE);
+  d_tsid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_SEP);
 
   // indicate we are using the default theory state object
   d_theoryState = &d_state;
@@ -1914,12 +1918,12 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, InferenceId id,
       if( conc==d_false ){
         Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << id
                            << std::endl;
-        d_im.conflictExp(id, ProofRule::THEORY_INFERENCE, ant, {conc});
+        d_im.conflictExp(id, ProofRule::TRUST, ant, {d_tiid, conc, d_tsid});
       }else{
         Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant
                            << " by " << id << std::endl;
-        TrustNode trn =
-            d_im.mkLemmaExp(conc, ProofRule::THEORY_INFERENCE, ant, {}, {conc});
+        TrustNode trn = d_im.mkLemmaExp(
+            conc, ProofRule::TRUST, ant, {}, {d_tiid, conc, d_tsid});
         d_im.addPendingLemma(
             trn.getNode(), id, LemmaProperty::NONE, trn.getGenerator());
       }
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 9f19469ead6..43c31e90a18 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -53,6 +53,10 @@ class TheorySep : public Theory {
   /** True node for predicates = false */
   Node d_false;
 
+  /** Trust id (for proofs) */
+  Node d_tiid;
+  Node d_tsid;
+
   //whether bounds have been initialized
   bool d_bounds_init;
 
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 9e052cb858d..1538c2deb85 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -16,6 +16,8 @@
 #include "theory/sets/inference_manager.h"
 
 #include "options/sets_options.h"
+#include "proof/trust_id.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -30,6 +32,8 @@ InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
+  d_tid = mkTrustId(TrustId::THEORY_INFERENCE);
+  d_tsid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_SETS);
 }
 
 bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
@@ -117,7 +121,7 @@ bool InferenceManager::assertSetsFact(Node atom,
 {
   Node conc = polarity ? atom : atom.notNode();
   return assertInternalFact(
-      atom, polarity, id, ProofRule::THEORY_INFERENCE, {exp}, {conc});
+      atom, polarity, id, ProofRule::TRUST, {exp}, {d_tid, conc, d_tsid});
 }
 
 void InferenceManager::assertInference(Node fact,
diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
index e6d5d902ba3..cc7abc36f5b 100644
--- a/src/theory/sets/inference_manager.h
+++ b/src/theory/sets/inference_manager.h
@@ -87,6 +87,8 @@ class InferenceManager : public InferenceManagerBuffered
   /** constants */
   Node d_true;
   Node d_false;
+  Node d_tid;
+  Node d_tsid;
   /**
    * Reference to the state object for the theory of sets. We store the
    * (derived) state here, since it has additional methods required in this
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 3a3a9bb55f3..2d196fda030 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -1065,11 +1065,12 @@ void InferProofCons::convert(InferenceId infer,
     // untrustworthy conversion, the argument of THEORY_INFERENCE is its
     // conclusion
     ps.d_args.clear();
+    ps.d_args.push_back(mkTrustId(TrustId::THEORY_INFERENCE));
     ps.d_args.push_back(conc);
     Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_STRINGS);
     ps.d_args.push_back(t);
     // use the trust rule
-    ps.d_rule = ProofRule::THEORY_INFERENCE;
+    ps.d_rule = ProofRule::TRUST;
   }
   if (TraceIsOn("strings-ipc-debug"))
   {
@@ -1184,7 +1185,7 @@ std::shared_ptr<ProofNode> InferProofCons::getProofFor(Node fact)
   {
     utils::flattenOp(Kind::AND, ec, exp);
   }
-  pf.addStep(fact, ProofRule::STRING_INFERENCE, exp, args);
+  pf.addStep(fact, ProofRule::MACRO_STRING_INFERENCE, exp, args);
   return pf.getProofFor(fact);
 }
 
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index de68d87ec65..b2388ed8a03 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -45,8 +45,8 @@ namespace strings {
  * called when we need to construct a proof node from an InferInfo.
  *
  * This class uses lazy proof reconstruction. Namely, the getProofFor method
- * returns applications of the rule STRING_INFERENCE, which store the arguments
- * to the proof conversion routine "convert" below.
+ * returns applications of the rule MACRO_STRING_INFERENCE, which store the
+ * arguments to the proof conversion routine "convert" below.
  */
 class InferProofCons : protected EnvObj, public ProofGenerator
 {
@@ -83,8 +83,8 @@ class InferProofCons : protected EnvObj, public ProofGenerator
    * It should be the case that a call was made to notifyFact(ii) where
    * ii.d_conc is fact in this SAT context.
    *
-   * This returns the appropriate application of STRING_INFERENCE so that it
-   * can be reconstructed if necessary during proof post-processing.
+   * This returns the appropriate application of MACRO_STRING_INFERENCE so that
+   * it can be reconstructed if necessary during proof post-processing.
    */
   std::shared_ptr<ProofNode> getProofFor(Node fact) override;
   /** Identify this generator (for debugging, etc..) */
@@ -99,8 +99,8 @@ class InferProofCons : protected EnvObj, public ProofGenerator
                                    bool isRev,
                                    const std::vector<Node>& exp);
   /**
-   * Pack arguments of a STRING_INFERENCE rule application in args. This proof
-   * rule stores the arguments to the convert method of this class below.
+   * Pack arguments of a MACRO_STRING_INFERENCE rule application in args. This
+   * proof rule stores the arguments to the convert method of this class below.
    */
   static void packArgs(Node conc,
                        InferenceId infer,
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 04662f67d76..ccdf5b40ca8 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -54,7 +54,7 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::STRING_CODE_INJ, this);
   pc->registerChecker(ProofRule::STRING_SEQ_UNIT_INJ, this);
   // trusted rule
-  pc->registerTrustedChecker(ProofRule::STRING_INFERENCE, this, 2);
+  pc->registerTrustedChecker(ProofRule::MACRO_STRING_INFERENCE, this, 2);
 }
 
 Node StringProofRuleChecker::checkInternal(ProofRule id,
@@ -526,7 +526,7 @@ Node StringProofRuleChecker::checkInternal(ProofRule id,
     AlwaysAssert(t[0].getType() == t[1].getType());
     return t[0].eqNode(t[1]);
   }
-  else if (id == ProofRule::STRING_INFERENCE)
+  else if (id == ProofRule::MACRO_STRING_INFERENCE)
   {
     Assert(args.size() >= 3);
     return args[0];
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 14394a0d54a..8792ead674a 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -867,8 +867,8 @@ TrustNode TheoryEngine::ppRewrite(TNode term,
     {
       Node proven = tskl.getProven();
       Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
-      d_lazyProof->addStep(
-          proven, ProofRule::THEORY_PREPROCESS_LEMMA, {}, {proven, tidn});
+      d_lazyProof->addTrustedStep(
+          proven, TrustId::THEORY_PREPROCESS_LEMMA, {}, {tidn});
       skl.d_lemma = TrustNode::mkTrustLemma(proven, d_lazyProof.get());
     }
   }
@@ -1258,8 +1258,7 @@ TrustNode TheoryEngine::getExplanation(TNode node)
         Node proven = texplanation.getProven();
         TheoryId tid = theoryOf(atom)->getId();
         Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
-        d_lazyProof->addStep(
-            proven, ProofRule::THEORY_LEMMA, {}, {proven, tidn});
+        d_lazyProof->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn});
         texplanation =
             TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get());
       }
@@ -1439,7 +1438,7 @@ void TheoryEngine::lemma(TrustNode tlemma,
       Assert(from != THEORY_LAST);
       // add theory lemma step to proof
       Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from);
-      d_lazyProof->addStep(lemma, ProofRule::THEORY_LEMMA, {}, {lemma, tidn});
+      d_lazyProof->addTrustedStep(lemma, TrustId::THEORY_LEMMA, {}, {tidn});
       // update the trust node
       tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
     }
@@ -1541,7 +1540,7 @@ void TheoryEngine::conflict(TrustNode tconflict,
         // add theory lemma step
         Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
         Node conf = tconflict.getProven();
-        d_lazyProof->addStep(conf, ProofRule::THEORY_LEMMA, {}, {conf, tidn});
+        d_lazyProof->addTrustedStep(conf, TrustId::THEORY_LEMMA, {}, {tidn});
       }
       // store the explicit step, which should come from a different
       // generator, e.g. d_tepg.
@@ -1924,7 +1923,7 @@ TrustNode TheoryEngine::getExplanation(
         Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl;
         // otherwise, trusted theory lemma
         Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(ttid);
-        lcp->addStep(proven, ProofRule::THEORY_LEMMA, {}, {proven, tidn});
+        lcp->addTrustedStep(proven, TrustId::THEORY_LEMMA, {}, {tidn});
       }
       std::vector<Node> pfChildren;
       pfChildren.push_back(trn.getNode());
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 88557854765..006a6bf8afa 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -18,6 +18,7 @@
 #include "options/proof_options.h"
 #include "proof/annotation_proof_generator.h"
 #include "proof/eager_proof_generator.h"
+#include "proof/trust_id.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/inference_id_proof_annotator.h"
 #include "theory/output_channel.h"
@@ -592,10 +593,11 @@ TrustNode TheoryInferenceManager::annotateId(const TrustNode& trn,
   // ensure we have a proof generator, make trusted theory lemma if not
   if (trn.getGenerator() == nullptr)
   {
+    Node tid = mkTrustId(TrustId::THEORY_LEMMA);
     Node tidn =
         builtin::BuiltinProofRuleChecker::mkTheoryIdNode(d_theory.getId());
     trna = d_defaultPg->mkTrustNode(
-        trn.getNode(), ProofRule::THEORY_LEMMA, {}, {lemma, tidn}, isConflict);
+        trn.getNode(), ProofRule::TRUST, {}, {tid, lemma, tidn}, isConflict);
   }
   d_iipa->setAnnotation(lemma, id);
   return d_apg->transform(trna, d_iipa.get());
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 6522bb5181d..540385ea4ef 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -67,6 +67,7 @@ TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine)
     ts.push_back(d_tpg.get());
     d_tspg.reset(new TConvSeqProofGenerator(
         pnm, ts, userContext(), "TheoryPreprocessor::sequence"));
+    d_tpid = mkTrustId(TrustId::THEORY_PREPROCESS);
   }
 }
 
@@ -191,13 +192,13 @@ TrustNode TheoryPreprocessor::preprocessLemmaInternal(
     // add the original proof to the lazy proof
     d_lp->addLazyStep(node.getProven(),
                       node.getGenerator(),
-                      ProofRule::THEORY_PREPROCESS_LEMMA);
+                      TrustId::THEORY_PREPROCESS_LEMMA);
     // only need to do anything if lemmap changed in a non-trivial way
     if (!CDProof::isSame(lemmap, lemma))
     {
       d_lp->addLazyStep(tplemma.getProven(),
                         tplemma.getGenerator(),
-                        ProofRule::THEORY_PREPROCESS,
+                        TrustId::THEORY_PREPROCESS,
                         true,
                         "TheoryEngine::lemma_pp");
       // ---------- from node -------------- from theory preprocess
@@ -408,7 +409,7 @@ Node TheoryPreprocessor::rewriteWithProof(Node term,
       Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
                          << term << " -> " << termr << std::endl;
       pg->addRewriteStep(
-          term, termr, ProofRule::REWRITE, {}, {term}, isPre, tctx);
+          term, termr, ProofRule::MACRO_REWRITE, {}, {term}, isPre, tctx);
     }
   }
   return termr;
@@ -486,7 +487,7 @@ void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
         options(), "tpp-debug", "TheoryPreprocessor::preprocessWithProof");
     // always use term context hash 0 (default)
     pg->addRewriteStep(
-        term, termr, trn.getGenerator(), isPre, ProofRule::ASSUME, true, tctx);
+        term, termr, trn.getGenerator(), isPre, TrustId::NONE, true, tctx);
   }
   else
   {
@@ -495,9 +496,9 @@ void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
     // small step trust
     pg->addRewriteStep(term,
                        termr,
-                       ProofRule::THEORY_PREPROCESS,
+                       ProofRule::TRUST,
                        {},
-                       {term.eqNode(termr)},
+                       {d_tpid, term.eqNode(termr)},
                        isPre,
                        tctx);
   }
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 8535bca82c5..28e32a5aedf 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -165,6 +165,8 @@ class TheoryPreprocessor : protected EnvObj
    * contexts.
    */
   RtfTermContext d_rtfc;
+  /** Trust id */
+  Node d_tpid;
   /**
    * Rewrite with proof, which stores a REWRITE step in pg if necessary
    * and returns the rewritten form of term.
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index db5ece2090e..771e3f60ad4 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -24,7 +24,7 @@ namespace theory {
 TrustSubstitutionMap::TrustSubstitutionMap(Env& env,
                                            context::Context* c,
                                            std::string name,
-                                           ProofRule trustId,
+                                           TrustId trustId,
                                            MethodId ids)
     : EnvObj(env),
       d_ctx(c),
@@ -114,7 +114,7 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x,
     // failed to rewrite, we add a trust step which assumes eq is provable
     // from proven, and proceed as normal.
     Trace("trust-subs") << "...failed to rewrite " << proven << std::endl;
-    d_tspb->addStep(ProofRule::TRUST_SUBS_EQ, {proven}, {eq}, eq);
+    d_tspb->addTrustedStep(TrustId::SUBS_EQ, {proven}, {}, eq);
   }
   Trace("trust-subs") << "...successful rewrite" << std::endl;
   solvePg->addSteps(*d_tspb.get());
@@ -232,7 +232,7 @@ std::shared_ptr<ProofNode> TrustSubstitutionMap::getProofFor(Node eq)
                             true))
   {
     // if we fail for any reason, we must use a trusted step instead
-    d_tspb->addStep(ProofRule::TRUST_SUBS_MAP, pfChildren, {eq}, eq);
+    d_tspb->addTrustedStep(TrustId::SUBS_MAP, pfChildren, {}, eq);
   }
   Trace("trust-subs-pf") << "...made steps" << std::endl;
   // -------        ------- from external proof generators
diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index 6d7b8f6802d..c8ece6c2765 100644
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -44,7 +44,7 @@ class TrustSubstitutionMap : protected EnvObj, public ProofGenerator
   TrustSubstitutionMap(Env& env,
                        context::Context* c,
                        std::string name = "TrustSubstitutionMap",
-                       ProofRule trustId = ProofRule::PREPROCESS_LEMMA,
+                       TrustId trustId = TrustId::PREPROCESS_LEMMA,
                        MethodId ids = MethodId::SB_DEFAULT);
   /** Gets a reference to the underlying substitution map */
   SubstitutionMap& get();
@@ -126,7 +126,7 @@ class TrustSubstitutionMap : protected EnvObj, public ProofGenerator
    * The placeholder trusted ProofRule identifier for calls to addSubstitution
    * that are not given proof generators.
    */
-  ProofRule d_trustId;
+  TrustId d_trustId;
   /** The method id for which form of substitution to apply */
   MethodId d_ids;
   /**
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 23ca8a31a00..0b2e9ab1007 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -1494,7 +1494,7 @@ Node EqProof::addToProof(CDProof* p,
       Trace("eqproof-conv")
           << "EqProof::addToProof: adding a trust flattening rewrite step\n";
       Node bridgeEq = conclusion.eqNode(d_node);
-      p->addStep(bridgeEq, ProofRule::TRUST_FLATTENING_REWRITE, {}, {bridgeEq});
+      p->addTrustedStep(bridgeEq, TrustId::FLATTENING_REWRITE, {}, {});
       p->addStep(d_node, ProofRule::EQ_RESOLVE, {conclusion, bridgeEq}, {});
     }
     else