Structural recursion over `Acc` fails

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Structurally recursive functions over Acc (and any other recursive subsingleton predicate) that produce non-Props fail. The main reason behind this is that auxiliary helpers (below and brecOn) for Acc have motives that only eliminate to Prop, like any other predicate, despite being able to be strengthened to eliminate to arbitrary sorts. A solution to this would be to generate the aforementioned helpers on subsingleton the same way they're generated for non-Prop types instead of the IndPredBelow machinery.

Context

This issue was discovered when trying to reconstruct some Rocq code for constructing a computable indefinite description choice over decidable predicates on natural numbers Rocq reference

Steps to Reproduce

variable (P : Nat → Prop)
def R (x y : Nat) : Prop := x = y + 1 ∧ ¬ P y
def witness_of_Acc [h : DecidablePred P] (a : Acc (R P) n) : {n : Nat // P n} :=
  match a with
  | .intro k ak =>
    match h k with
      | isTrue h => ⟨k,h⟩
      | isFalse h =>
        witness_of_Acc (ak (k+1) ⟨rfl, h⟩)
termination_by structural a

Expected behavior: No error

Actual behavior:

failed to infer structural recursion:
Cannot use parameter a:
  brecOn is type incorrect
    Application type mismatch: The argument
      fun {n} a => funType_1 a
    has type
      {n : Nat} → Acc (R P) n → Type
    of sort `Type 1` but is expected to have type
      (a : Nat) → Acc (R P) a → Prop
    of sort `Type` in the application
      @Acc.brecOn Nat (R P) fun {n} a => funType_1 a

Versions

Lean 4.30.0-nightly-2026-02-28 Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the minimal Lean example for witness_of_Acc and inspect the Acc.brecOn and below helpers involved in structural recursion. Compare their IndPredBelow generation with helper generation for non-Prop types. Done means the example compiles while preserving the intended recursive subsingleton behavior.