Method try_proof_irrel

crates/kernel/src/def_eq.rs:800–817

Proof irrelevance: if both are proofs of propositions (types in Prop), they're def-eq. We check type(type(a)) = Sort(0), meaning type(a) : Prop. The "is `a_ty` propositional?" question is delegated to [`Self::is_prop_type`], which caches by the type's content hash so a repeat probe on the same proposition skips the recursive `infer ∘ whnf` chain entirely. Without that cache, every successful proo

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

    if matches!(a.data(), ExprData::Str(..))
      || matches!(b.data(), ExprData::Str(..))
    {
      if self.try_string_lit_expansion(a, b)? {
        return Ok(true);
      }
      if self.try_string_lit_expansion(b, a)? {
        return Ok(true);
      }
    }

    // Struct eta + unit-like + proof irrelevance fallback
    if self.try_eta_struct(a, b)? {
      return Ok(true);
    }
    if self.try_eta_struct(b, a)? {
      return Ok(true);
    }
    if self.try_def_eq_unit(a, b)? {
      return Ok(true);
    }
    self.try_proof_irrel(a, b)
  }