datatype IntList where
| Cons(Int, IntList)
| Nil
end

function reverse(xs: IntList) -> IntList
begin
    reverse_help(xs, Nil)
end

function reverse_help(xs: IntList, ys: IntList) -> IntList
begin
    match xs with
    | Nil => ys
    | Cons(head, tail) => reverse_help(tail, Cons(head, ys))
    end
end

function rev_nat_list(n: Int) -> IntList
begin
    if n == 0 then
        Nil
    else
        Cons(n, rev_nat_list(n - 1))
end

function reverse_backward(xs: IntList)
begin
    fresh ys;
    guard ys = rev_nat_list(100);
    guard ys = reverse(xs);
end

query reverse_backward(depth_step=50, depth_limit=1000, answer_limit=1)