872def lifetimesInsert =
873 (lambda unrestricted lifetime : (family Lifetime) .
874 (lambda unrestricted ordered : (family Lifetimes) .
875 (eliminate
876 Lifetimes
877 (lambda unrestricted current : (family Lifetimes) . (family Lifetimes))
878 ordered
879 (branch
880 LifetimesEnd
881 .
882 (constructor Lifetimes LifetimesNext lifetime (constructor Lifetimes LifetimesEnd)))
883 (branch
884 LifetimesNext
885 head
886 tail
887 ih_tail
888 .
889 (nat-eliminate
890 (lambda unrestricted before : Nat . (family Lifetimes))
891 (constructor Lifetimes LifetimesNext head ih_tail)
892 (lambda unrestricted predecessor : Nat .
893 (lambda unrestricted induction : (family Lifetimes) .
894 (constructor Lifetimes LifetimesNext lifetime ordered)))
895 (lifetimeComesBeforeOrEqual lifetime head))))))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.