Axioms and Classes disagree on parametricity

In the Type Classes chapter we can read "Lean does not allow case analysis of types" and "polymorphic functions implement operations that are uniform for any choice of type argument":
https://github.com/leanprover/reference-manual/blob/5d2a1e3c97acc754de5b9751efd6d13ba6666530/Manual/Classes.lean#L42

In the Axioms chapter we can read "parametricity is [...] not compatible with Lean's standard axioms":
https://github.com/leanprover/reference-manual/blob/5d2a1e3c97acc754de5b9751efd6d13ba6666530/Manual/Axioms.lean#L74

It also has an example that does case analysis on whether a type is Nat
https://github.com/leanprover/reference-manual/blob/5d2a1e3c97acc754de5b9751efd6d13ba6666530/Manual/Axioms.lean#L90

I believe the intent in the Type Classes chapter was for computable functions only (in particular functions that don't use the axiom of choice). But the text as currently written is a bit misleading (since it doesn't mention computability or the absence of axiom of choice explicitly).

Start by comparing the cited passages in Manual/Classes.lean and Manual/Axioms.lean, especially the lines linked in the issue. Clarify the Type Classes discussion so its claim about uniform polymorphic functions is scoped consistently with the axiom-of-choice and computability context, then verify that the two chapters no longer appear contradictory.