Method replace_aux_refs_for_sort

crates/kernel/src/inductive.rs:759–878

Rewrite nested occurrences in synthetic aux member/ctor types to the corresponding synthetic aux constants before running `sort_consts` partition refinement. Compile-side `expand_nested_block` does this via its queue pass over all expanded constructors; the kernel has already discovered the flat aux set, so it can rewrite by matching each occurrence against that set.

(
    &mut self,
    e: &KExpr<M>,
    aux: &[FlatBlockMember<M>],
    aux_ids: &[KId<M>],
    block_us: &[KUniv<M>],
    n_block_params: u64,
    local_depth: u64,
  )

        own_params: ext_params,
        n_indices: ext_indices,
        ctors: ext_ctors,
        lvls: ext_lvls,
        ind_us: aux_us,
        occurrence_us,
      });
      Ok(())
    })();
    self.lctx.truncate(saved_lctx);
    result
  }

  /// Rewrite nested occurrences in synthetic aux member/ctor types to the
  /// corresponding synthetic aux constants before running `sort_consts`
  /// partition refinement. Compile-side `expand_nested_block` does this via
  /// its queue pass over all expanded constructors; the kernel has already
  /// discovered the flat aux set, so it can rewrite by matching each
  /// occurrence against that set.
  fn replace_aux_refs_for_sort(
    &mut self,
    e: &KExpr<M>,
    aux: &[FlatBlockMember<M>],
    aux_ids: &[KId<M>],
    block_us: &[KUniv<M>],
    n_block_params: u64,
    local_depth: u64,
  ) -> Result<KExpr<M>, TcError<M>> {
    if let Some(replaced) = self.try_replace_aux_ref_for_sort(
      e,
      aux,
      aux_ids,
      block_us,
      n_block_params,
      local_depth,
    )? {
      return Ok(replaced);
    }

    let result = match e.data() {
      ExprData::App(f, a, _) => {
        let f2 = self.replace_aux_refs_for_sort(
          f,
          aux,
          aux_ids,
          block_us,
          n_block_params,
          local_depth,
        )?;
        let a2 = self.replace_aux_refs_for_sort(
          a,
          aux,
          aux_ids,
          block_us,
          n_block_params,
          local_depth,
        )?;
        KExpr::app(f2, a2)
      },
      ExprData::Lam(n, bi, ty, body, _) => {