280def arenaRangesEqual =
281 (lambda unrestricted a : (family ArenaRanges) . (lambda unrestricted b : (family ArenaRanges) .
282 (app
283 (eliminate ArenaRanges (lambda unrestricted c : (family ArenaRanges) . (pi unrestricted other : (family ArenaRanges) . Nat)) a
284 (branch ArenaRangesNone . (lambda unrestricted other : (family ArenaRanges) . (arenaRangesEmpty other)))
285 (branch ArenaRangesNext start stop rest induction . (lambda unrestricted other : (family ArenaRanges) .
286 (eliminate ArenaRanges (lambda unrestricted c : (family ArenaRanges) . Nat) other
287 (branch ArenaRangesNone . 0)
288 (branch ArenaRangesNext s2 e2 t2 i2 .
289 (naturalAnd (naturalAnd (naturalEqual start s2) (naturalEqual stop e2)) (induction t2)))))))
290 b)))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.