Theorems proved by well-founded recursion get labelled @[irreducible]. While this is mostly invisible in VSCode, it shows up in doc-gen and is confusing to users.

Problem

When a theorem is proved using well-founded recursion, it receives an @[irreducible] annotation as a side effect. This annotation is visible in doc-gen output and is confusing, since users don't expect theorems to carry reducibility annotations.

Possible solutions

• If theorems don't actually need the @[irreducible] annotation, stop adding it.
• If the annotation is necessary internally, consider a doc-gen level solution:
  • Hide the @[irreducible] attribute on theorems in doc-gen.
  • Or add a tooltip explaining that it is a side effect of well-founded recursion and not user-specified.