2 files changed, 36 insertions, 10 deletions
diff --git a/include/atp/infer/substitution.h b/include/atp/infer/substitution.h
index f9f562a..671f6d7 100644
--- a/include/atp/infer/substitution.h
+++ b/include/atp/infer/substitution.h
@@ -16,39 +16,61 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file substitution.h
 /// @brief Variable binding map: Var -> Term.
+///
+/// Short-lived object created during unification, applied to build resolvents,
+/// then discarded. Never stored long-term.
 
+#include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 
-#include <vector>
+#include <unordered_map>
 
 namespace atp {
 
-/// A substitution is a mapping from variable TermIds to their bound TermIds.
-/// Designed as a short-lived, stack-allocated object during unification.
+/// A substitution σ maps variable TermIds to their bound TermIds.
+///
+/// Example: σ = { X → f(a), Y → Z }
+///   lookup(X) = f(a)     (direct binding)
+///   resolve(X) = f(a)    (same — f(a) is not a variable)
+///   resolve(Y) = Z       (if Z is unbound, stops at Z)
+///   resolve(Y) = f(b)    (if Z → f(b) also in σ, walks the chain)
 class Substitution {
   public:
     Substitution() = default;
 
-    /// Bind a variable to a term. Returns false if already bound to something different.
+    /// Bind a variable to a term. Returns false if already bound to a different term.
     bool bind(TermId var, TermId term);
 
-    /// Look up what a variable is bound to. Returns kInvalidId if unbound.
+    /// Look up what a variable is directly bound to. Returns kInvalidId if unbound.
     [[nodiscard]] TermId lookup(TermId var) const;
 
-    /// Walk the binding chain to the final bound value.
-    [[nodiscard]] TermId resolve(TermId id) const;
+    /// Walk the binding chain to the final value.
+    /// If var → Y → f(a), returns f(a).
+    /// Requires TermBank to check whether intermediate values are variables.
+    [[nodiscard]] TermId resolve(TermId id, const TermBank& bank) const;
+
+    /// Apply this substitution to a term recursively, creating new terms in the bank.
+    /// Free (unbound) variables are left as-is.
+    [[nodiscard]] TermId apply(TermId term, TermBank& bank) const;
+
+    /// Check if a variable occurs anywhere inside a term (for occurs check).
+    [[nodiscard]] bool occursIn(TermId var, TermId term, const TermBank& bank) const;
 
     /// Clear all bindings.
     void clear();
 
+    /// Number of bindings.
+    [[nodiscard]] size_t size() const { return bindings_.size(); }
+
+    /// Check if empty.
+    [[nodiscard]] bool empty() const { return bindings_.empty(); }
+
   private:
-    // TODO: Phase 2 implementation
-    std::vector<std::pair<TermId, TermId>> bindings_;
+    std::unordered_map<TermId, TermId> bindings_;
 };
 
 }  // namespace atp
diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h
index 7d91aaf..f2ea180 100644
--- a/include/atp/infer/unification.h
+++ b/include/atp/infer/unification.h
@@ -37,4 +37,8 @@ struct UnificationConfig {
 bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
            const UnificationConfig& config = {});
 
+/// Apply a substitution to a term recursively, creating new terms in the bank.
+/// Free (unbound) variables are left unchanged.
+TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank);
+
 }  // namespace atp