Genesis committee.
As explained in committees, there is an arbitrary but fixed genesis committee, which we capture via a constrained nullary function.
Theorem: committeep-of-genesis-committee
(defthm committeep-of-genesis-committee (committeep (genesis-committee)))
