(VAR L N IL M) (RULES zeros -> cons(0) U101(tt) -> U102(isNatKind) U102(tt) -> U103(isNatIListKind) U103(tt) -> U104(isNatIListKind) U104(tt) -> U105(isNat) U105(tt) -> U106(isNatIList) U106(tt) -> tt U11(tt) -> U12(isNatIListKind) U111(tt) -> U112(isNatIListKind) U112(tt) -> U113(isNat) U113(tt) -> U114(isNatKind) U114(tt) -> s(length(L)) U12(tt) -> U13(isNatList) U121(tt) -> U122(isNatIListKind) U122(tt) -> nil U13(tt) -> tt U131(tt) -> U132(isNatIListKind) U132(tt) -> U133(isNat) U133(tt) -> U134(isNatKind) U134(tt) -> U135(isNat) U135(tt) -> U136(isNatKind) U136(tt) -> cons(N) U21(tt) -> U22(isNatKind) U22(tt) -> U23(isNat) U23(tt) -> tt U31(tt) -> U32(isNatIListKind) U32(tt) -> U33(isNatList) U33(tt) -> tt U41(tt) -> U42(isNatKind) U42(tt) -> U43(isNatIListKind) U43(tt) -> U44(isNatIListKind) U44(tt) -> U45(isNat) U45(tt) -> U46(isNatIList) U46(tt) -> tt U51(tt) -> U52(isNatIListKind) U52(tt) -> tt U61(tt) -> U62(isNatIListKind) U62(tt) -> tt U71(tt) -> tt U81(tt) -> tt U91(tt) -> U92(isNatKind) U92(tt) -> U93(isNatIListKind) U93(tt) -> U94(isNatIListKind) U94(tt) -> U95(isNat) U95(tt) -> U96(isNatList) U96(tt) -> tt isNat -> tt isNat -> U11(isNatIListKind) isNat -> U21(isNatKind) isNatIList -> U31(isNatIListKind) isNatIList -> tt isNatIList -> U41(isNatKind) isNatIListKind -> tt isNatIListKind -> tt isNatIListKind -> U51(isNatKind) isNatIListKind -> U61(isNatKind) isNatKind -> tt isNatKind -> U71(isNatIListKind) isNatKind -> U81(isNatKind) isNatList -> tt isNatList -> U91(isNatKind) isNatList -> U101(isNatKind) length(nil) -> 0 length(cons(N)) -> U111(isNatList) take(0,IL) -> U121(isNatIList) take(s(M),cons(N)) -> U131(isNatIList) )