diff --git a/base/src/main/java/org/aya/base/core/AppTerm.java b/base/src/main/java/org/aya/base/core/AppTerm.java
index f2061b85..a4f55cee 100644
--- a/base/src/main/java/org/aya/base/core/AppTerm.java
+++ b/base/src/main/java/org/aya/base/core/AppTerm.java
@@ -10,4 +10,12 @@ public record AppTerm(@NotNull Term fun, @NotNull Term arg) implements Term {
     if (newFun == fun && newArg == arg) return this;
     return new AppTerm(newFun, newArg);
   }
+
+  @Override public @NotNull Term replace(int index, @NotNull Term incoming) {
+    var newArg = arg.replace(index, incoming);
+    var newFun = fun.replace(index, incoming);
+    if (newFun instanceof LamTerm(var body)) return body.instantiate(incoming);
+    if (newFun == fun && newArg == arg) return this;
+    return new AppTerm(newFun, newArg);
+  }
 }
diff --git a/base/src/main/java/org/aya/base/core/FreeTerm.java b/base/src/main/java/org/aya/base/core/FreeTerm.java
index 66ec8214..308fb811 100644
--- a/base/src/main/java/org/aya/base/core/FreeTerm.java
+++ b/base/src/main/java/org/aya/base/core/FreeTerm.java
@@ -8,4 +8,8 @@ public record FreeTerm(@NotNull LocalVar name) implements Term {
     if (name == var) return new LocalTerm(depth);
     return this;
   }
+
+  @Override public @NotNull Term replace(int index, @NotNull Term arg) {
+    return this;
+  }
 }
diff --git a/base/src/main/java/org/aya/base/core/LamTerm.java b/base/src/main/java/org/aya/base/core/LamTerm.java
index ed305758..f7b02269 100644
--- a/base/src/main/java/org/aya/base/core/LamTerm.java
+++ b/base/src/main/java/org/aya/base/core/LamTerm.java
@@ -1,5 +1,6 @@
 package org.aya.base.core;
 
+import kala.collection.mutable.MutableList;
 import org.aya.base.generic.LocalVar;
 import org.jetbrains.annotations.NotNull;
 
@@ -9,4 +10,10 @@ public record LamTerm(Term body) implements Term {
     if (newBody == body) return this;
     return new LamTerm(newBody);
   }
+
+  @Override public @NotNull Term replace(int index, @NotNull Term arg) {
+    var newBody = body.replace(index + 1, arg);
+    if (newBody == body) return this;
+    return new LamTerm(newBody);
+  }
 }
diff --git a/base/src/main/java/org/aya/base/core/LocalTerm.java b/base/src/main/java/org/aya/base/core/LocalTerm.java
index b1deb123..3316a098 100644
--- a/base/src/main/java/org/aya/base/core/LocalTerm.java
+++ b/base/src/main/java/org/aya/base/core/LocalTerm.java
@@ -7,4 +7,9 @@ public record LocalTerm(int index) implements Term {
   @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
     return this;
   }
+
+  @Override public @NotNull Term replace(int incoming, @NotNull Term arg) {
+    if (index == incoming) return arg;
+    return this;
+  }
 }
diff --git a/base/src/main/java/org/aya/base/core/Term.java b/base/src/main/java/org/aya/base/core/Term.java
index 09faa86e..f0c6d342 100644
--- a/base/src/main/java/org/aya/base/core/Term.java
+++ b/base/src/main/java/org/aya/base/core/Term.java
@@ -7,11 +7,32 @@
 import java.io.Serializable;
 
 public sealed interface Term extends Serializable
-    permits AppTerm, FreeTerm, LamTerm, LocalTerm {
+  permits AppTerm, FreeTerm, LamTerm, LocalTerm {
   @ApiStatus.Internal
   @NotNull Term bindAt(@NotNull LocalVar var, int depth);
 
+  /**
+   * Corresponds to <emph>abstract</emph> operator in [MM 2004].
+   * However, <code>abstract</code> is a keyword in Java, so we can't
+   * use it as a method name.
+   * <pre>
+   * abstract :: Name → Expr → Scope
+   * </pre>
+   *
+   * @see #instantiate
+   */
   default @NotNull Term bind(@NotNull LocalVar var) {
     return bindAt(var, 0);
   }
+
+  @ApiStatus.Internal
+  @NotNull Term replace(int index, @NotNull Term arg);
+
+  /**
+   * Corresponds to <emph>instantiate</emph> operator in [MM 2004].
+   * Could be called <code>apply</code>
+   */
+  default @NotNull Term instantiate(Term arg) {
+    return replace(0, arg);
+  }
 }