261def arenaEventsShifted =
262 (lambda unrestricted shift : Nat .
263 (lambda unrestricted earlier : (family ArenaEvents) . (lambda unrestricted later : (family ArenaEvents) .
264 (app
265 (eliminate ArenaEvents
266 (lambda unrestricted current : (family ArenaEvents) . (pi unrestricted other : (family ArenaEvents) . Nat))
267 earlier
268 (branch ArenaEventsEnd . (lambda unrestricted other : (family ArenaEvents) .
269 (eliminate ArenaEvents (lambda unrestricted c : (family ArenaEvents) . Nat) other
270 (branch ArenaEventsEnd . 1) (branch ArenaEventsNext h t i . 0))))
271 (branch ArenaEventsNext head rest induction . (lambda unrestricted other : (family ArenaEvents) .
272 (eliminate ArenaEvents (lambda unrestricted c : (family ArenaEvents) . Nat) other
273 (branch ArenaEventsEnd . 0)
274 (branch ArenaEventsNext h t i . (naturalAnd (arenaEventShifted shift head h) (induction t)))))))
275 later))))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.