(VAR F n x xs y ys )
(RULES 
        foldr(F, x, nil) -> x
        foldr(F, x, cons(y, ys)) -> 
        length(xs) -> foldr(, 0, xs)
        
)