refactor: expose operation-first ITree carrier

[dtumad]

Summary

• define ITree.Poly F α reducibly as F + C α + X
• represent ITree as a one-field wrapper around the raw M-type, with definitionally inverse ofM/toM maps and equivM
• retain the ergonomic Shape API through ViewPoly and migrate corecursion, coinduction, simulations, and event interpreters to it
• align Resumption and DynComputation with the operation-first p + C β convention
• add representation canaries and update the ITree and polynomial-functor documentation

This follows the representation pattern explored in leanprover/cslib#731 while retaining the current cslib dependency pin.

Validation

• ./scripts/validate.sh --lint --test