(VAR IL L M N T )
(RULES 
        uTake2(tt) -> cons(N)
        uLength(tt) -> s(length(L))
        and(tt,T) -> T
        isNatIList -> isNatList
        isNat -> tt
        isNat -> isNat
        isNat -> isNatList
        isNatIList -> tt
        isNatIList -> and(isNat,isNatIList)
        isNatList -> tt
        isNatList -> and(isNat,isNatList)
        isNatList -> and(isNat,isNatIList)
        zeros -> cons(0)
        take(0,IL) -> uTake1(isNatIList)
        uTake1(tt) -> nil
        take(s(M),cons(N)) -> uTake2(and(isNat,and(isNat,isNatIList)))
        length(cons(N)) -> uLength(and(isNat,isNatList))
        
)