diff --git a/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java b/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java
index 44c029a1fb..a8a00a73d8 100644
--- a/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.tycker;
 
@@ -77,19 +77,7 @@ public sealed interface TeleTycker extends Contextful {
    */
   @Contract(mutates = "param2")
   static void bindTele(ImmutableSeq<LocalVar> binds, MutableSeq<Param> tele) {
-    final var lastIndex = tele.size() - 1;
-    // fix some param, say [p]
-    // we skip the last parameter, which need no binds
-    for (int i = lastIndex - 1; i >= 0; i--) {
-      var p = binds.get(i);
-      // for any other param that is able to refer to [p]
-      for (int j = i + 1; j < tele.size(); j++) {
-        var og = tele.get(j);
-        // j - i is the human distance between [p] and [og]. However, we count from 0
-        int ii = i, jj = j;
-        tele.set(j, og.descent(x -> x.bindAt(p, jj - ii - 1)));
-      }
-    }
+    tele.replaceAllIndexed((i, p) -> p.descent(t -> t.bindTele(binds.sliceView(0, i))));
   }
 
   @Contract(mutates = "param3")
diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitCon.java b/syntax/src/main/java/org/aya/syntax/compile/JitCon.java
index 6f7b177c2e..43002c7b3f 100644
--- a/syntax/src/main/java/org/aya/syntax/compile/JitCon.java
+++ b/syntax/src/main/java/org/aya/syntax/compile/JitCon.java
@@ -76,6 +76,6 @@ protected JitCon(
       this.selfTele = selfTele.toImmutableSeq();
     }
 
-    return Param.substTele(selfTele.view(), ownerArgs.view()).toImmutableSeq();
+    return Param.instTele(selfTele.view(), ownerArgs.view()).toImmutableSeq();
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ConDef.java b/syntax/src/main/java/org/aya/syntax/core/def/ConDef.java
index 451003aa74..d9f85b0581 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ConDef.java
+++ b/syntax/src/main/java/org/aya/syntax/core/def/ConDef.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.def;
 
@@ -55,7 +55,7 @@ public static final class Delegate extends TyckAnyDef<ConDef> implements ConDefL
     @Override public int selfTeleSize() { return core().selfTele.size(); }
     @Override public int ownerTeleSize() { return core().ownerTele.size(); }
     @Override public @NotNull ImmutableSeq<Param> selfTele(@NotNull ImmutableSeq<Term> ownerArgs) {
-      return Param.substTele(core().selfTele.view(), ownerArgs.view()).toImmutableSeq();
+      return Param.instTele(core().selfTele.view(), ownerArgs.view()).toImmutableSeq();
     }
 
     @Override public @NotNull DataDefLike dataRef() { return core().dataRef; }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java
index 0b6ed20c7c..94fc2dc59c 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/FreeTerm.java
@@ -1,7 +1,8 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.term;
 
+import kala.collection.immutable.ImmutableSeq;
 import kala.function.IndexedFunction;
 import org.aya.syntax.core.term.marker.TyckInternal;
 import org.aya.syntax.ref.LocalVar;
@@ -10,8 +11,16 @@
 public record FreeTerm(@NotNull LocalVar name) implements TyckInternal {
   public FreeTerm(@NotNull String name) { this(LocalVar.generate(name)); }
   @Override public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) { return this; }
-  @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
-    if (name == var) return new LocalTerm(depth);
-    return this;
+  // @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
+  //   if (name == var) return new LocalTerm(depth);
+  //   return this;
+  // }
+
+  @Override public @NotNull Term bindAllFrom(@NotNull ImmutableSeq<LocalVar> vars, int fromDepth) {
+    var idx = vars.indexOf(this.name);
+    if (idx == -1) return this;
+
+    var realDepth = fromDepth + idx;
+    return new LocalTerm(realDepth);
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.java
index 1313889efd..992b23b3bc 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/LocalTerm.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.term;
 
@@ -12,14 +12,8 @@ public record LocalTerm(int index) implements Term {
     assert index >= 0 : "Sanity check";
   }
 
-  @Override
-  public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
-    return this;
-  }
-
-  @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
-    return this;
-  }
+  @Override public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) { return this; }
+  @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) { return this; }
 
   @Override public @NotNull Term replaceAllFrom(int from, @NotNull ImmutableSeq<Term> list) {
     var i = index - from;
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Param.java b/syntax/src/main/java/org/aya/syntax/core/term/Param.java
index 32da559af1..7f0e1dd573 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/Param.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/Param.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.term;
 
@@ -17,7 +17,7 @@
 import java.util.function.UnaryOperator;
 
 public record Param(@NotNull String name, @NotNull Term type, boolean explicit) implements AyaDocile {
-  public static @NotNull SeqView<Param> substTele(SeqView<Param> tele, SeqView<Term> subst) {
+  public static @NotNull SeqView<Param> instTele(SeqView<Param> tele, SeqView<Term> subst) {
     return tele.mapIndexed((idx, p) -> p.descent(ty -> ty.instTeleFrom(idx, subst)));
   }
 
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Term.java b/syntax/src/main/java/org/aya/syntax/core/term/Term.java
index a8db3a88ad..a2efa3aaab 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/Term.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/Term.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.core.term;
 
@@ -34,7 +34,16 @@ public sealed interface Term extends Serializable, AyaDocile
   }
 
   default @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
-    return descent((i, t) -> t.bindAt(var, depth + i));
+    return bindAllFrom(ImmutableSeq.of(var), depth);
+  }
+
+  /// Bind all [LocalVar] since `fromDepth`,
+  /// the i-th [LocalVar] in `vars` will be replaced by a [LocalTerm] with index `fromDepth + i`.
+  ///
+  /// @see #replaceAllFrom
+  default @NotNull Term bindAllFrom(@NotNull ImmutableSeq<LocalVar> vars, int fromDepth) {
+    if (vars.isEmpty()) return this;
+    return descent((i, t) -> t.bindAllFrom(vars, fromDepth + i));
   }
 
   /**
@@ -60,17 +69,17 @@ public sealed interface Term extends Serializable, AyaDocile
    */
   default @NotNull Term bindTele(int depth, @NotNull SeqView<LocalVar> teleVars) {
     if (teleVars.isEmpty()) return this;
-    return teleVars.reversed().foldLeftIndexed(this,
-      (idx, acc, var) -> acc.bindAt(var, depth + idx));
+    return bindAllFrom(teleVars.reversed().toImmutableSeq(), depth);
   }
 
   default @NotNull Term bindTele(@NotNull SeqView<LocalVar> teleVars) {
     return bindTele(0, teleVars);
   }
 
-  /**
-   * Replacing indexes from {@code from} to {@code from + list.size()} (exclusive) with {@code list}
-   */
+  /// Replacing indexes from `from` to `from + list.size()` (exclusive) with `list`,
+  /// a [LocalTerm] with index `from + i` will be replaced by `list[i]` if possible.
+  ///
+  /// @see #bindAllFrom
   @ApiStatus.Internal
   default @NotNull Term replaceAllFrom(int from, @NotNull ImmutableSeq<Term> list) {
     if (list.isEmpty()) return this;