diff --git a/core/src/core_check_module.rs b/core/src/core_check_module.rs
index 90cf0c2..f3dacca 100644
--- a/core/src/core_check_module.rs
+++ b/core/src/core_check_module.rs
@@ -674,9 +674,32 @@ fn register_inductive(
     // `StructFields::inductive_paths`'s doc comment for why inserting it
     // into `known_globals` (which also feeds `open`-based unqualified-name
     // aliasing) is the wrong place for this.
+    let inductive_atom = atoms.intern(ind.name().clone());
     structs
       .inductive_paths
-      .insert(atoms.intern(ind.name().clone()), ind.name().clone());
+      .insert(inductive_atom, ind.name().clone());
+    // An ordinary inductive's own bare name (`I64`, `Bool`, `List`) was
+    // never given a `ctx` (kind) entry either, for the same "never
+    // needed before" reason as the `known_globals` gap just above — but
+    // unlike that one, this DOES matter for genuinely dependent explicit
+    // Pi telescopes (`def f (A : Type) (a : A) : ...`), where a concrete
+    // type like `I64`/`Bool` is passed as an ordinary VALUE argument for
+    // `A` and needs its own kind (`Type`/`Sort n`) inferred to check that
+    // argument — without this, `infer`ring `Free(inductive_atom)` here
+    // always failed with `UnboundVariable`, the second half of the
+    // `Eq.rec`/dependent-Pi bug (see `plans/implementations/evaluator-
+    // recursion-and-eq-rec-followup.md`, Part 3 Fix A — this fix and the
+    // `pi_named_with_mult` one are both needed together). `ind.typ()` is
+    // the inductive's own declared kind (its own param `Pi`-chain ending
+    // in `Sort n`/`Prop`/`Type`, e.g. `Sort 1 -> A -> A -> Prop` for
+    // `Eq`) — lowered the same way a constructor's own type is, just
+    // above.
+    if let Ok(kind_c) = lower_term(
+      &mut LowerContext::with_config(config.clone(), atoms),
+      ind.typ(),
+    ) {
+      ctx.insert(inductive_atom, kind_c);
+    }
     // E2: every ordinary constructor's own field types, in declaration
     // order, still referencing the inductive's own declared params freely
     // (NOT yet substituted with any specific use site's concrete type
@@ -2891,6 +2914,72 @@ mod test {
     assert_eq!(report.passed(), 1);
   }
 
+  // -------------------------------------------------------------------
+  // Dependent explicit Pi telescopes — `plans/implementations/
+  // evaluator-recursion-and-eq-rec-followup.md`, Part 3 Fix A. Before
+  // this fix, a LATER explicit param's declared type referencing an
+  // EARLIER explicit param's name (e.g. `(a : A)` after `(A : Type)`)
+  // failed with `type mismatch: <unknown> vs. <unknown>` at the DEF
+  // site — root cause: `parser.rs`'s `def`-param-list desugaring built
+  // each param's `Pi` via `pi_with_mult`, which always set
+  // `arg_name: None`, so `lower_core.rs`'s `Term::Pi` lowering had no
+  // name to push into scope for a later domain to reference via
+  // `Bound` (unlike `Term::Forall`, which always carries a real name).
+  // A SEPARATE, second fix was needed for the APPLICATION side: an
+  // ordinary inductive's own bare name (`Bool`, `I64`) used as a VALUE
+  // argument (not just a type annotation) had no `ctx` kind entry
+  // (`core_check_module.rs`'s ordinary-inductive registration) and no
+  // runtime `GlobalDef` (`lower_core_ir.rs`), plus `unify` needed a
+  // narrow special case treating the "Type" keyword's `Free` reference
+  // as interchangeable with a raw `Sort` literal (bare "Type" surface
+  // syntax, unlike explicit "Sort N", resolves to `Free(atom)` via
+  // ordinary name lookup, not directly to `CoreTerm::Sort`).
+  // -------------------------------------------------------------------
+
+  #[test]
+  fn test_dependent_explicit_pi_telescope_definition_checks() {
+    // A later explicit param's type referencing an earlier one, even
+    // when the body never uses that later param at all (isolates the
+    // signature-checking bug from any body-checking concern).
+    let env = ModuleCheckEnv::new();
+    let report = check_module_source(&env, "def id_ty (A : Type) (a : A) : A := a\n");
+    assert_eq!(report.defs.len(), 1);
+    assert!(
+      report.defs[0].result.is_ok(),
+      "expected pass, got {:?}",
+      report.defs[0].result
+    );
+  }
+
+  #[test]
+  fn test_dependent_explicit_pi_telescope_application_checks() {
+    // Applying such a function to a concrete type VALUE (`I64`), not
+    // just declaring it — exercises the application-side fix
+    // (`core_check_module.rs`'s inductive kind registration,
+    // `core_unify.rs`'s Sort-keyword special case) on top of the
+    // definition-side one above.
+    let env = ModuleCheckEnv::new();
+    let report = check_module_source(
+      &env,
+      "def id_ty (A : Type) (a : A) : A := a\ndef applied : I64 := id_ty I64 5\n",
+    );
+    assert_eq!(report.passed(), 2, "report: {report:?}");
+  }
+
+  #[test]
+  fn test_dependent_explicit_pi_telescope_over_gadt_index_checks() {
+    // The harder case from the same investigation: a `Vec (len : Nat) A`
+    // GADT-indexed argument, where the dependency is carried through an
+    // inductive's own declared index rather than a bare type variable.
+    let env = ModuleCheckEnv::new();
+    let report = check_module_source(
+      &env,
+      "def dep (n : Nat) (v : Vec n I64) : I64 := 0\n\
+       def applied : I64 := dep Nat.zero Vec.nil\n",
+    );
+    assert_eq!(report.passed(), 2, "report: {report:?}");
+  }
+
   #[test]
   fn test_harness_supports_recursive_def() {
     // A def whose body calls itself (matches the shape of most real
diff --git a/core/src/core_unify.rs b/core/src/core_unify.rs
index cacc4a6..48c337d 100644
--- a/core/src/core_unify.rs
+++ b/core/src/core_unify.rs
@@ -423,6 +423,36 @@ pub fn unify(mctx: &mut MetaContext, a: &CoreTerm, b: &CoreTerm) -> Result<(), U
       }
     }
 
+    // Bare "Type"/"Prop"/"Pred" surface syntax (unlike explicit "Sort N")
+    // doesn't lower to a raw `Sort` literal — it falls through ordinary
+    // name resolution to `Free(atom)`, since `core_check_module.rs`'s own
+    // registration loop (see its "E7" comment) deliberately also gives
+    // these three atoms an ordinary `ctx` entry so they're usable as
+    // plain VALUES too (`get_sort Type`), not just as type annotations.
+    // That split means a dependent explicit Pi telescope (`def f (A :
+    // Type) (a : A) : ...`) has `A`'s declared param type as
+    // `Free(type_atom)`, while a concrete type's OWN inferred kind
+    // (`I64`/`Bool`'s registered `ctx` entry, `core_check_module.rs`'s
+    // ordinary-inductive registration) is a raw `Sort { level: 1 }` — two
+    // different representations of the identical concept, which plain
+    // structural unification (the `Free`-vs-`Free`/`Sort`-vs-`Sort` cases
+    // above) can't see through. Recognize the three well-known keyword
+    // atoms here and apply the SAME cumulativity rule (E7 above) as if
+    // they'd been the raw `Sort` they stand for — narrowly scoped to
+    // exactly these three atoms, not a general "unfold any global" rule.
+    (CoreTerm::Sort { level: l1 }, CoreTerm::Free(atom)) => {
+      match known_sort_keyword_level(mctx, *atom) {
+        Some(l2) if *l1 <= l2 => Ok(()),
+        _ => Err(mismatch(a, b)),
+      }
+    }
+    (CoreTerm::Free(atom), CoreTerm::Sort { level: l2 }) => {
+      match known_sort_keyword_level(mctx, *atom) {
+        Some(l1) if l1 <= *l2 => Ok(()),
+        _ => Err(mismatch(a, b)),
+      }
+    }
+
     (
       CoreTerm::Forall {
         typ: t1, body: b1, ..
@@ -504,6 +534,22 @@ pub fn unify(mctx: &mut MetaContext, a: &CoreTerm, b: &CoreTerm) -> Result<(), U
   }
 }
 
+/// If `atom` is one of the three well-known "Type"/"Prop"/"Pred" keyword
+/// atoms (`core_check_module.rs`'s "E7" registration loop), the `Sort`
+/// level it stands for — `Type` -> 1, `Prop`/`Pred` -> 0 (`Pred` is a
+/// plain alias for `Prop`), matching `sort_parser`'s own "Sort N" ->
+/// `Sort { level: N }` convention exactly, just reached through a name
+/// lookup instead of a literal. `None` for any other atom — this is
+/// deliberately narrow (three specific, well-known global names), not a
+/// general "does this atom's value happen to be a Sort" unfolding.
+fn known_sort_keyword_level(mctx: &MetaContext, atom: Atom) -> Option<u64> {
+  match mctx.atoms().path_of(atom)?.to_string().as_str() {
+    "Type" => Some(1),
+    "Prop" | "Pred" => Some(0),
+    _ => None,
+  }
+}
+
 fn mismatch(left: CoreTerm, right: CoreTerm) -> UnifyError {
   UnifyError::Mismatch {
     left: Arc::new(left),
diff --git a/core/src/lower_core_ir.rs b/core/src/lower_core_ir.rs
index 971d378..02debe9 100644
--- a/core/src/lower_core_ir.rs
+++ b/core/src/lower_core_ir.rs
@@ -1044,6 +1044,27 @@ pub fn lower_program(program: &CoreProgram) -> Result<LoweredProgram, LowerCoreI
       globals.push(GlobalDef::Def(std::sync::Arc::new(CoreIr::Lit(
         IrLit::Sort(level),
       ))));
+    } else if program.inductives.contains_key(path) {
+      // The identical gap as `builtin_sort_level` just above, for an
+      // ORDINARY inductive's own bare name (`Bool`, `I64`, `List`) used
+      // as a VALUE — needed once a genuinely dependent explicit Pi
+      // telescope (`def f (A : Type) (a : A) : ...`) is actually CALLED
+      // with a concrete type argument (`f Bool true`), not just declared
+      // — `core_check_module.rs`'s own inductive registration now gives
+      // these a `ctx` (kind) entry for type-checking (see its own doc
+      // comment there), but nothing gave them a RUNTIME representation
+      // until now, so evaluating one hit `UnresolvedGlobal` even once
+      // checking passed. Defaults to `Sort(1)` (`Type`) — correct for
+      // every ordinary data inductive; a `: Prop` (`Sort 0`) inductive's
+      // own BARE name (e.g. plain `Eq`, not an applied `Eq A a b`) used
+      // as a value would get the wrong level here, a narrow, accepted
+      // gap (this program's own `CoreInductiveInfo` doesn't carry the
+      // inductive's declared level to recover it precisely, and nothing
+      // in the `Eq.rec`/dependent-Pi work this fixes ever references a
+      // bare, unapplied `Eq` as a value).
+      globals.push(GlobalDef::Def(std::sync::Arc::new(CoreIr::Lit(
+        IrLit::Sort(1),
+      ))));
     } else {
       // A bare reference with no def, instance, or constructor behind
       // it at all — in practice this is a class method's own abstract
diff --git a/core/src/parser.rs b/core/src/parser.rs
index cb0ae95..73e975e 100644
--- a/core/src/parser.rs
+++ b/core/src/parser.rs
@@ -23,7 +23,7 @@ use crate::{
     match_term,
     module::ParsedModule,
     mpvar, num_suffix, opr, param, param_with_attrs, param_with_default, param_with_mult, pi_name,
-    pi_typs, pi_with_mult, pvar, stru, stru_field_to_def_param, stru_field_with_mult,
+    pi_named_with_mult, pi_typs, pvar, stru, stru_field_to_def_param, stru_field_with_mult,
     type_constraint, var_id,
   },
 };
@@ -1627,7 +1627,12 @@ fn def_parser(input: Span) -> Res<Def> {
   } else {
     let mut full_typ = return_typ;
     for param in plain_params.iter().rev() {
-      full_typ = pi_with_mult((*param.typ).clone(), full_typ, param.mult.clone());
+      full_typ = pi_named_with_mult(
+        param.name.clone(),
+        (*param.typ).clone(),
+        full_typ,
+        param.mult.clone(),
+      );
     }
     if !implicit_params.is_empty() {
       full_typ = foralls(implicit_params, full_typ);
diff --git a/core/src/parser/test/declarations.rs b/core/src/parser/test/declarations.rs
index 7fcba83..24e2810 100644
--- a/core/src/parser/test/declarations.rs
+++ b/core/src/parser/test/declarations.rs
@@ -574,7 +574,11 @@ fn test_instance() {
       vec![def(
         mpt("map"),
         vec![],
-        pi(pi(typ("A"), typ("B")), pi(app2("F", "A"), app2("F", "B"))),
+        pi_var(
+          id("f"),
+          pi(typ("A"), typ("B")),
+          pi_var(id("v"), app2("F", "A"), app2("F", "B"))
+        ),
         lams(
           vec![dpar("f", pi(typ("A"), typ("B"))), dpar("v", app2("F", "A"))],
           oper(var("f"), "|>", var("v"))
@@ -695,7 +699,7 @@ fn test_def() {
       vec![type_constraint(mpt("Monad"), vec![id("M")])],
       forall(
         dpar("M", pi(typ("Type"), typ("Type"))),
-        pi(app2("M", "String"), app2("M", "Unit"))
+        pi_var(id("arg"), app2("M", "String"), app2("M", "Unit"))
       ),
       lams(
         vec![dpar("arg", app2("M", "String"))],
@@ -719,7 +723,7 @@ fn test_def() {
     def(
       mpt("main"),
       vec![],
-      pi(app2("List", "String"), app2("IO", "Unit")),
+      pi_var(id("args"), app2("List", "String"), app2("IO", "Unit")),
       lams(
         vec![dpar("args", app2("List", "String"))],
         apps(var("println"), vec![str("Hello, world!")])
@@ -755,9 +759,18 @@ fn test_def() {
     def(
       mpt("Lens"),
       vec![type_constraint(mpt("Functor"), vec![id("F")])],
-      pi_typs(
-        vec![typ("Type"), typ("Type"), typ("Type"), typ("Type")],
-        typ("Type")
+      pi_var(
+        id("S"),
+        typ("Type"),
+        pi_var(
+          id("T"),
+          typ("Type"),
+          pi_var(
+            id("A"),
+            typ("Type"),
+            pi_var(id("B"), typ("Type"), typ("Type"))
+          )
+        )
       ),
       lams(
         vec![
@@ -824,7 +837,11 @@ fn module_test() {
       decl_def(
         mpt("append"),
         vec![],
-        pi(app2("List", "A"), pi(app2("List", "A"), app2("List", "A"))),
+        pi_var(
+          id("a"),
+          app2("List", "A"),
+          pi_var(id("b"), app2("List", "A"), app2("List", "A"))
+        ),
         lams(
           vec![dpar("a", app2("List", "A")), dpar("b", app2("List", "A"))],
           var("todo"),
diff --git a/core/src/parser/test/do_notation.rs b/core/src/parser/test/do_notation.rs
index 939fb5f..5dcb296 100644
--- a/core/src/parser/test/do_notation.rs
+++ b/core/src/parser/test/do_notation.rs
@@ -208,7 +208,7 @@ fn test_def_do_block_with_params() {
     def(
       mpt("greet"),
       vec![],
-      pi(typ("String"), app2("IO", "Unit")),
+      pi_var(id("name"), typ("String"), app2("IO", "Unit")),
       lams(
         vec![dpar("name", typ("String"))],
         apps(var("println"), vec![var("name")])
@@ -356,7 +356,7 @@ fn test_def_do_block_with_constraints() {
       vec![type_constraint(mpt("Monad"), vec![id("M")])],
       forall(
         dpar("M", pi(typ("Type"), typ("Type"))),
-        pi(app2("M", "String"), app2("M", "Unit"))
+        pi_var(id("arg"), app2("M", "String"), app2("M", "Unit"))
       ),
       lams(
         vec![dpar("arg", app2("M", "String"))],
diff --git a/core/src/parser/test/docstrings.rs b/core/src/parser/test/docstrings.rs
index 4d98677..37f4737 100644
--- a/core/src/parser/test/docstrings.rs
+++ b/core/src/parser/test/docstrings.rs
@@ -13,7 +13,7 @@ def add (a b: I64) : I64 := a + b
     def(
       mpt("add"),
       vec![],
-      pi(typ("I64"), pi(typ("I64"), typ("I64"))),
+      pi_var(id("a"), typ("I64"), pi_var(id("b"), typ("I64"), typ("I64"))),
       lams(
         vec![dpar("a", typ("I64")), dpar("b", typ("I64"))],
         expected_body
@@ -131,9 +131,10 @@ instance Functor List {
       vec![def(
         mpt("map"),
         vec![],
-        pi(
+        pi_var(
+          id("f"),
           pi(typ("A"), typ("B")),
-          pi(app2("List", "A"), app2("List", "B"))
+          pi_var(id("v"), app2("List", "A"), app2("List", "B"))
         ),
         lams(
           vec![
diff --git a/core/src/term.rs b/core/src/term.rs
index eefec5e..18f8a24 100644
--- a/core/src/term.rs
+++ b/core/src/term.rs
@@ -1126,6 +1126,27 @@ pub fn pi_with_mult(arg: Term, ret: Term, mult: Multiplicity) -> Term {
     mult,
   }
 }
+/// Same as `pi_with_mult`, but also threads the parameter's real name
+/// through as `arg_name` — needed so a LATER parameter's type can refer
+/// to an EARLIER one by name (e.g. `def f (A : Type) (a : A) : ...`).
+/// `lower_core.rs`'s `Term::Pi` lowering arm pushes `arg_name` into scope
+/// before lowering `ret`, exactly like `Term::Forall`'s `name` already
+/// does for implicit parameters — `pi_with_mult`'s `arg_name: None`
+/// leaves nothing to push, so a later param's type-level reference to an
+/// earlier one falls through to free-name resolution instead of a
+/// `Bound` reference, independently (and inconsistently) on the type
+/// side vs. the body's own `Term::Lam` chain (which DOES carry real
+/// names) — see `def_param_names`'s doc comment for the historical
+/// context, and `plans/implementations/evaluator-recursion-and-eq-rec-
+/// followup.md` (Part 3, Fix A) for the bug this fixes.
+pub fn pi_named_with_mult(name: Identifier, arg: Term, ret: Term, mult: Multiplicity) -> Term {
+  Term::Pi {
+    arg_name: Some(name),
+    arg: Box::new(arg),
+    ret: Box::new(ret),
+    mult,
+  }
+}
 pub fn pi_name(arg_name: Option<Identifier>, arg: Term, ret: Term) -> Term {
   Term::Pi {
     arg_name,