(STRATEGY
    INNERMOST)

(VAR
    x y)
(DATATYPES
    A = µX.< Cons(X, X), Nil >)
(SIGNATURES
    letexp :: [A x A] -> A
    goal :: [A x A] -> A)
(RULES
    letexp(x,y) ->
      letexp(Cons(Cons(Nil(),Nil()),x)
            ,y)
    goal(x,y) -> letexp(x,y))