datatype List[a] where
| Nil
| Cons(a, List[a])
end
function concat[a](xs: List[a], ys: List[a]) -> List[a]
begin
match xs with
| Nil => ys
| Cons(head, tail) => Cons(head, concat(tail, ys))
end
end
function rev_nat_list(n: Int) -> List[Int]
begin
if n == 0 then Nil
else Cons(n, rev_nat_list(n - 1))
end
function example(zs: List[Int])
begin
guard concat(rev_nat_list(100), rev_nat_list(100)) = zs;
end
query example(depth_step=50, depth_limit=1000, answer_limit=1)