Method try_unfold_proj_app

crates/kernel/src/def_eq.rs:1535–1545

If the head of `e` is a projection, try reducing it via whnf_no_delta. Returns the reduced form if it changed, None otherwise (lean4lean tryUnfoldProjApp).

(
    &mut self,
    e: &KExpr<M>,
  )

        *a = self.whnf_core(&a2)?;
      } else {
        return Ok(LazyDeltaStep::Unknown);
      }
    } else if !a_delta && b_delta {
      if let Some(a2) = self.try_unfold_proj_app(a)? {
        *a = a2;
      } else if let Some(b2) = self.delta_unfold_one(b)? {
        *b = self.whnf_core(&b2)?;
      } else {
        return Ok(LazyDeltaStep::Unknown);
      }
    } else {
      let a_id = a_head.as_ref().expect("a_delta implies head");
      let b_id = b_head.as_ref().expect("b_delta implies head");
      let cmp = self.def_rank_id(a_id)?.cmp(&self.def_rank_id(b_id)?);