658def coppeliusTiledSchedulesAdmitted : Nat =
659 (eliminate StdList (lambda unrestricted c : (family StdList (family CoppeliusTiledShape)) . Nat) coppeliusTiledShapes
660 (branch StdListEmpty . 1)
661 (branch StdListCons head tail induction . (naturalAnd (coppeliusTiledShapeAdmitted head) induction)))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.