(VAR k l l' s s' t t' x x' y z )
(RULES 
        and(true, y) -> y
        and(false, y) -> false
        eq(nil, nil) -> true
        eq(cons(t, l), nil) -> false
        eq(nil, cons(t, l)) -> false
        eq(cons(t, l), cons(t', l')) -> and(eq(t, t'), eq(l, l'))
        eq(var(l), var(l')) -> eq(l, l')
        eq(var(l), apply(t, s)) -> false
        eq(var(l), lambda(x, t)) -> false
        eq(apply(t, s), var(l)) -> false
        eq(apply(t, s), apply(t', s')) -> and(eq(t, t'), eq(s, s'))
        eq(apply(t, s), lambda(x, t)) -> false
        eq(lambda(x, t), var(l)) -> false
        eq(lambda(x, t), apply(t, s)) -> false
        eq(lambda(x, t), lambda(x', t')) -> and(eq(x, x'), eq(t, t'))
        if(true, var(k), var(l')) -> var(k)
        if(false, var(k), var(l')) -> var(l')
        ren(var(l), var(k), var(l')) -> if(eq(l, l'), var(k), var(l'))
        ren(x, y, apply(t, s)) -> apply(ren(x, y, t), ren(x, y, s))
        ren(x, y, lambda(z, t)) -> lambda(var(cons(x, cons(y, cons(lambda(z, t), nil)))), ren(x, y, ren(z, var(cons(x, cons(y, cons(lambda(z, t), nil)))), t)))
        
)