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
    | Cons(head, tail) => reverse_help(tail, Cons(head, ys))
    | Nil => ys
    end
end

function length(xs: IntList) -> Int
begin
    match xs with
    | Cons(_, tail) => length(tail) + 1
    | Nil => 0
    end
end

function same_length_after_reverse(xs: IntList)
begin
    guard length(reverse(xs)) != length(xs);
end

query same_length_after_reverse(depth_step=5, depth_limit=50, answer_limit=1)