(VAR x xs )
(RULES 
        isList(nil) -> tt
        isList(Cons(x, xs)) -> isList(xs)
        downfrom(0) -> nil
        downfrom(s(x)) -> Cons(s(x), downfrom(x))
        f(x) -> cond(isList(downfrom(x)), s(x))
        cond(tt, x) -> f(x)
        
)