(** In this file, you will fill in the details in the proof of *Girard's paradox*, as described in
Martin-Lof's 1972 "An intuitionistic theory of types", which thwarted Martin-Lof's original plan
for a type theory having "Type-in-Type".
The proof is a replication of the classic "Burali-Forti" paradox showing (like Russell's paradox)
the problem with a naive theory of sets in which one does not distinguish between "set" and
"proper class"; it shows that the set of all ordinals cannot itself be a set. The idea is to show
that the set of all ordinals would itself be an ordinal, and from this to derive a contradiction.
Here, an *ordinal* is the "order-type" (i.e. equivalence class under order-preserving isomorphisms)
of a *well-order*, where a *well-order* is a linear order having no infinite descending sequences of
elements.
One simplification in Girard's paradox is that "well-ordering" is replaced by "well-founded relation".
Here is the classical Burali-Forti paradox, with this simplification.
A *well-founded relation* on a set A is defined to be a binary relation <⊆A×A such that there does
not exist a sequence aₙ∈A such that aₙ₊₁