A hierarchy exists for a nonempty count with a nonzero fan-out, and the
role must be one of its participants.
216def participantTreeAdmitted =
217 (lambda unrestricted fanout : Nat .
218 (lambda unrestricted count : Nat .
219 (lambda unrestricted role : Nat .
220 (naturalAnd
221 (naturalNonzero fanout)
222 (naturalAnd (naturalNonzero count) (naturalLess role count))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.