(VAR k x x' xs xs' y ys )
(STRATEGY INNERMOST)
(RULES 
        @(Cons(x,xs),ys) -> Cons(x,@(xs,ys))
        @(Nil,ys) -> ys
        binom(Cons(x,xs),Cons(x',xs')) -> @(binom(xs,xs'),binom(xs,Cons(x',xs')))
        binom(Cons(x,xs),Nil) -> Cons(Nil,Nil)
        binom(Nil,k) -> Cons(Nil,Nil)
        goal(x,y) -> binom(x,y)
        
)