diff --git a/base/src/main/java/org/aya/tyck/TyckState.java b/base/src/main/java/org/aya/tyck/TyckState.java
index 404792b6..ee2c06c1 100644
--- a/base/src/main/java/org/aya/tyck/TyckState.java
+++ b/base/src/main/java/org/aya/tyck/TyckState.java
@@ -2,13 +2,12 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
-import kala.collection.mutable.MutableList;
-import org.aya.syntax.core.term.Term;
+import org.aya.syntax.ref.DeBruijnCtx;
 import org.aya.syntax.ref.LocalCtx;
 import org.jetbrains.annotations.NotNull;
 
 public record TyckState(
   @NotNull LocalCtx ctx,
-  @NotNull MutableList<Term> dCtx
+  @NotNull DeBruijnCtx dCtx
   ) {
 }
diff --git a/base/src/main/java/org/aya/tyck/tycker/StateBased.java b/base/src/main/java/org/aya/tyck/tycker/StateBased.java
index 09bed59e..2392822f 100644
--- a/base/src/main/java/org/aya/tyck/tycker/StateBased.java
+++ b/base/src/main/java/org/aya/tyck/tycker/StateBased.java
@@ -2,16 +2,8 @@
 // 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;
 
-import org.aya.generic.Modifier;
-import org.aya.syntax.concrete.stmt.decl.TeleDecl;
-import org.aya.syntax.core.def.FnDef;
-import org.aya.syntax.core.def.TeleDef;
 import org.aya.syntax.core.term.*;
-import org.aya.syntax.core.term.call.Callable;
-import org.aya.syntax.ref.DefVar;
-import org.aya.tyck.Result;
 import org.aya.tyck.TyckState;
-import org.aya.util.Arg;
 import org.jetbrains.annotations.NotNull;
 
 /**
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/SigmaTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/SigmaTerm.java
index 4167f7b4..e15f146e 100644
--- a/syntax/src/main/java/org/aya/syntax/core/term/SigmaTerm.java
+++ b/syntax/src/main/java/org/aya/syntax/core/term/SigmaTerm.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 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;
 
diff --git a/syntax/src/main/java/org/aya/syntax/ref/DeBruijnCtx.java b/syntax/src/main/java/org/aya/syntax/ref/DeBruijnCtx.java
new file mode 100644
index 00000000..60dc3f62
--- /dev/null
+++ b/syntax/src/main/java/org/aya/syntax/ref/DeBruijnCtx.java
@@ -0,0 +1,43 @@
+// Copyright (c) 2020-2024 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.ref;
+
+import kala.collection.mutable.MutableList;
+import org.aya.syntax.core.term.Term;
+import org.aya.util.error.InternalException;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.function.Supplier;
+
+/**
+ * It is NOT DeBrujin
+ *
+ * @param ctx reversed ctx, the last one is the type of 0.
+ */
+public record DeBruijnCtx(@NotNull MutableList<Term> ctx) {
+  /**
+   * Maps {@code 0} to {@code type}
+   */
+  public void push(@NotNull Term type) {
+    ctx.append(type);
+  }
+
+  public @NotNull Term get(int index) {
+    if (index < 0) throw new InternalException("index < 0");
+    if (index >= ctx.size()) throw new InternalException("index >= ctx.size()");
+    var realIndex = ctx.size() - 1 - index;
+    return ctx.get(realIndex);
+  }
+
+  public <R> @NotNull R with(@NotNull Term type, @NotNull Supplier<R> subscope) {
+    push(type);
+    var ret = subscope.get();
+    pop();
+    return ret;
+  }
+
+  public @NotNull Term pop() {
+    if (ctx.isEmpty()) throw new InternalException("empty ctx");
+    return ctx.removeLast();
+  }
+}