diff --git a/base/.gitignore b/base/.gitignore
new file mode 100644
index 00000000..00597b17
--- /dev/null
+++ b/base/.gitignore
@@ -0,0 +1,4 @@
+build
+.gradle
+src/main/gen
+src/main/resources/META-INF/native-image
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 b78c8bf6..f2061b85 100644
--- a/base/src/main/java/org/aya/base/core/AppTerm.java
+++ b/base/src/main/java/org/aya/base/core/AppTerm.java
@@ -5,6 +5,9 @@
 
 public record AppTerm(@NotNull Term fun, @NotNull Term arg) implements Term {
   @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
-    return new AppTerm(fun.bindAt(var, depth), arg.bindAt(var, depth));
+    var newFun = fun.bindAt(var, depth);
+    var newArg = arg.bindAt(var, depth);
+    if (newFun == fun && newArg == arg) return this;
+    return new AppTerm(newFun, newArg);
   }
 }
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 bc8d4e87..ed305758 100644
--- a/base/src/main/java/org/aya/base/core/LamTerm.java
+++ b/base/src/main/java/org/aya/base/core/LamTerm.java
@@ -5,6 +5,8 @@
 
 public record LamTerm(Term body) implements Term {
   @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
-    return new LamTerm(body.bindAt(var, depth + 1));
+    var newBody = body.bindAt(var, depth + 1);
+    if (newBody == body) return this;
+    return new LamTerm(newBody);
   }
 }