Revamp the set theory library

[dhalilov]

This PR ports parts of the set theory library we have to the new kernel, using more automation and reducing the size of proofs.

A lot of files were split and re-organized for better organization and discoverability. Here is the new tree:

├── Base
├── Functions
│   ├── Examples
│   └── Operations
├── Order
│   ├── Examples
│   └── WellOrders
├── Ordinals
├── Relations
│   ├── Examples
│   └── Operations
└── Types
    └── ADT

It also adds the following features:

• Move to Unicode-based syntax, including set-builder notations {x ∈ y | φ(x)} and {f(x) | x ∈ y}
• Custom printers using printAs
• A sectioning mechanism using section, useful for printing
• Some bug fixes for Congruence
• Predef files for quick exports
• Run a pre-defined list of theories in the CI

Things left to port:

• Some basic theorems about ordinals (TransfiniteInduction relies on them)
• Some theorems about well-orders and initial segments
• WellOrderedRecursion, uniqueness is proven but existence is missing since the proof constructs the function by hand
• ADTs
• GroupTheory
• RingTheory
• TopologyTheory

(Note: the diff contains parts of @SimonGuilloud's port to the new kernel, hence the number of files affected is huge.)

[SimonGuilloud]

Looks good!

[SimonGuilloud]

It seems there is an issue with your ci.yml file:
https://github.com/epfl-lara/lisa/actions/runs/16078339248
that prevents the ci from running

[SimonGuilloud]

ci fails :(

[SimonGuilloud]

Merging; some issues remain including a dotty bug that occurs only when typed application is used in a different porject than the definition, and another bug related to patern matching.