Introduction
Working in an untyped set theory in higher order logic, some of the things already available as typed constructions have to
be reworked in this untyped universe of sets.
In higher order logic arbitrary tuples are available as typed constructions by iterating the typed ordered pair constructor,
and lists are separately available.
Both are desirable because the tuples are of fixed length determined by their type, but can have components of distinct types,
while lists are of arbitrary length but must be of uniform type.
In the set theory things work our differently.
Lists are themselves more easily constructed (and this can be done using the ordered pair constructor) and are not restrained
by a type system (within the set theory).
Ordered tuples are less useful in this context and are probably superfluous if lists are available.

Cons and nil
We can use the ordered pair constructor and the empty set for the list constructor and the empty list, but, just in case we
want to differentiate between pairs and lists in the proof automation I will give them new names.
xlholconst nil : GS

nil = ∅_{g}

xlholconst cons : GS → GS → GS

∀h t• cons h t = h ↦_{g} t



The List Constructor
We can borrow a bit of the special syntax for lists in HOL by providing a list (set) constructor which takes a HOL list (of
sets) as its argument.
xlholconst list : GS LIST → GS

∀h t• list [] = nil ∧ list (Cons h t) = cons h (list t)


Destructors
Having adopted new names for existing constructors we now do the same for the destructors.
xlholconst head tail: GS → GS

head = fst
∧ tail = snd

To which we add a numeric selector.
xlholconst nth : ℕ → GS → GS

∀n l• nth 0 l = head l
∧ nth (n+1) l = nth n (tail l)


