experiment: forbid large elim of recursive Prop inductives

[nomeata]

This PR is an experiment that restricts Acc.rec and other recursors
for recursive Prop inductives to motives in Prop, removing large
elimination for them while preserving it for non-recursive
subsingleton-style products like Eq, And, Iff, Or, and Unit.
The motivation is to ensure the kernel never has to look at a proof
term of a Prop, which would in turn enable downstream tooling (e.g.
external checkers) to drop proof subterms after typechecking.

This is not intended for merging as-is: it is a snapshot to measure
the cost (in stdlib churn and in performance) of imposing the
restriction, so we can decide whether to pursue it further.

elim_only_at_universe_zero in src/kernel/inductive.cpp now returns
true for is_rec() inductives. WellFounded.fix is redefined in
Init/WF.lean via a recursive Prop FixGraph relation plus
Classical.choice from the prelude (avoiding the import cycle that
would arise from import Init.Classical). Init/WFComputable.lean is
restructured: Acc.recC/Acc.ndrec and their csimp pairs are removed
(the recursor signature no longer matches), but compilable csimp rules
for WellFounded.fixF and WellFounded.fix are restored and proved
via FixGraph uniqueness. Init/While.lean's whileM.fix is
rewritten on top of WellFounded.fixF with an explicit unfolding
lemma.

Test expectations adjusted: casesOnAcc.lean is dropped (it tested
large elimination of Acc.casesOn into Nat, which is exactly what
the restriction removes), print_cmd.lean's #print Acc.rec snapshot
is updated to the restricted signature, csimpCore.lean no longer
lists (Acc.rec, Acc.recC), and kernelBacktrack.lean now sees
Classical.choice in the axiom dependency list.

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com