Fix singleton extraction after implicit erasure

[JiaJunDeng5930]

Fixes #22348

Summary

• Classify singleton inductives from constructor fields that remain after logical erasure and Extraction Implicit.
• Reuse the same constructor-field filter when producing the extracted inductive packets.
• Add regression coverage for constructor applications, pattern matches, parameter offsets, and the existing SafeImplicits diagnostic.

Root cause

extract_really_ind only excluded logical fields when deciding whether an inductive used the Singleton representation. extract_inductive later also removed fields declared through Extraction Implicit. Erasing the sole field could therefore leave a Singleton with no payload, violating the assumptions in constructor and match lowering.

When no field remains, the corrected classification uses the Standard representation. Code that does not depend on the erased field now extracts as a nullary constructor; code that still depends on it reaches the existing SafeImplicits error.

Testing

• opam exec -- dune exec --root . rocq -- compile -q -bt test-suite/bugs/bug_22348.v

• The same focused command passed for test-suite/success/extraction_impl.v, test-suite/bugs/bug_11114.v, and test-suite/bugs/bug_13581.v.

• git diff --check

• Added / updated test-suite.

[JiaJunDeng5930]

@coqbot run full ci

[coqbot-app]

Sorry, @JiaJunDeng5930, I only accept requests from members of the @rocq-prover/contributors team. If you are a regular contributor, you can request to join the team by asking any core developer.

[ppedrot]

@coqbot run full ci