Method try_same_head_spine

crates/kernel/src/def_eq.rs:606–635

Same-head constant: if both are `C us args`, compare spines without unfolding.

(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  )

      | (
        ExprData::All(name, bi, ty1, body1, _),
        ExprData::All(_, _, ty2, body2, _),
      ) => {
        if !self.is_def_eq(ty1, ty2)? {
          return Ok(false);
        }
        // Open both bodies with the SAME fresh fvar — the common-fvar
        // trick that makes alpha-renamed bodies hash-equal under
        // `instantiate_rev` and lets def-eq compare them structurally.
        // Mirrors lean4lean `isDefEqBinding`
        // (refs/lean4lean/Lean4Lean/TypeChecker.lean:546).
        self.with_lctx_scope(|tc| {
          let fv_id = tc.fresh_fvar_id();
          let fv = tc.intern(KExpr::fvar(fv_id, name.clone()));
          tc.lctx.push(
            fv_id,
            LocalDecl::CDecl {
              name: name.clone(),
              bi: bi.clone(),
              ty: ty1.clone(),
            },
          );
          let b1_open = instantiate_rev(
            &mut tc.env.intern,
            body1,
            std::slice::from_ref(&fv),
          );
          let b2_open = instantiate_rev(&mut tc.env.intern, body2, &[fv]);
          tc.is_def_eq(&b1_open, &b2_open)
        })
      },
      _ => Ok(false),
    }
  }