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 intlist_eq(xs: IntList, ys: IntList) -> Bool
begin
    match xs with
    | Cons(head, tail) => match ys with
        | Cons(head2, tail2) => head == head2 && intlist_eq(tail, tail2)
        | Nil => false
        end
    | Nil => match ys with
        | Cons(_head2, _tail2) => false
        | Nil => true
        end
    end
end

function double_reverse_same(xs: IntList)
begin
    guard !intlist_eq(reverse(reverse(xs)), xs);
end

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