(VAR a k ls x )
(RULES 
        rev(ls) -> r1(ls, empty)
        r1(empty, a) -> a
        r1(cons(x, k), a) -> r1(k, cons(x, a))
        
)