(datatype list
    (Cons i64 list))
(function EmptyConst () list)
(let Empty (EmptyConst))

(relation eq (list list))

(eq Empty Empty)

; Oddly, this version works:
; (rule ((= x (Cons x1 rest1)) (= y (Cons x2 rest2)) (= 0 (- x1 x2)) (eq rest1 rest2))
(rule ((= x (Cons x1 rest1)) (= y (Cons x2 rest2)) (= x1 x2) (eq rest1 rest2))
      ((eq (Cons x1 rest1) (Cons x2 rest2))))

(let mylist (Cons 1 Empty))

(run 100)