Method build_minor_at_depth

crates/kernel/src/inductive.rs:2597–2807

Build minor premise type for a constructor, called while params and motives are already on the context. This makes de Bruijn indices correct. For constructor `C : ∀ params fields, I params indices`: ```text ∀ (f₁ : F₁) ... (fₙ : Fₙ) (ih₁ : ∀ xs, motive(indices(rec_field₁ xs), rec_field₁ xs)) ... (ihₘ : ∀ xs, motive(indices(rec_fieldₘ xs), rec_fieldₘ xs)), motive(ctor_indices, C params f₁...fₙ) ``

(
    &mut self,
    ind_idx: usize,
    ctor_id: &KId<M>,
    member: &FlatBlockMember<M>,
    n_rec_params: usize,
    motive_base: usize, // context level where motives start
    flat: &[FlatBlockM

      // major scope.
      let lift_by = u64_to_usize::<M>(depth)?;
      for sp in member.spec_params.iter() {
        let lifted = if lift_by > 0 {
          lift(&mut self.env.intern, sp, lift_by as u64, 0)
        } else {
          sp.clone()
        };
        major_ty = self.intern(KExpr::app(major_ty, lifted));
      }
    }
    // Apply indices (the index binders we're about to wrap around).
    for i in 0..n_idx {
      let v = self.intern(KExpr::var((n_idx - 1 - i) as u64, anon()));
      major_ty = self.intern(KExpr::app(major_ty, v));
    }

    // Build: ∀ (major : major_ty), Sort elim_level
    let sort = self.intern(KExpr::sort(elim_level.clone()));
    let mut result =
      self.intern(KExpr::all(anon(), bi_default(), major_ty, sort));

    // Wrap with index foralls (from inside out).
    for i in (0..n_idx).rev() {
      result = self.intern(KExpr::all(
        anon(),
        bi_default(),
        index_doms[i].clone(),
        result,
      ));
    }

    Ok(result)
  }

  /// Build minor premise type for a constructor, called while params and motives
  /// are already on the context. This makes de Bruijn indices correct.
  ///
  /// For constructor `C : ∀ params fields, I params indices`:
  /// ```text
  /// ∀ (f₁ : F₁) ... (fₙ : Fₙ)
  ///   (ih₁ : ∀ xs, motive(indices(rec_field₁ xs), rec_field₁ xs))
  ///   ...
  ///   (ihₘ : ∀ xs, motive(indices(rec_fieldₘ xs), rec_fieldₘ xs)),
  ///   motive(ctor_indices, C params f₁...fₙ)
  /// ```
  fn build_minor_at_depth(
    &mut self,
    ind_idx: usize,
    ctor_id: &KId<M>,
    member: &FlatBlockMember<M>,
    n_rec_params: usize,
    motive_base: usize, // context level where motives start
    flat: &[FlatBlockMember<M>],
    block_addrs: &[Address],
    _univ_offset: u64,
  ) -> Result<KExpr<M>, TcError<M>> {
    let ctor = match self.get_const(ctor_id)? {
      KConst::Ctor { ty, lvls, .. } => (ty.clone(), lvls),
      _ => {