;; Timeout (alors qu'il devrait trouver un contrex)
(set-logic HORN)


(declare-datatypes ((elt 0) (eltlist 0)) 
	(
		(
			(a) 
			(b)
		)
		(
			(nil)
			(cons (hd elt) (tl eltlist))
		)
	)
)


(define-fun-rec append ((l1 eltlist) (l2 eltlist)) eltlist 
	(
		match l1
		(
			(nil l2)
			((cons h1 t1) (cons h1 (append t1 l2)))
		)
	)
)

(define-fun-rec reverse ((l1 eltlist)) eltlist
	(
		match l1
		(
			(nil nil)
			((cons h1 t1) (append (reverse t1) (cons h1 nil)))
		)
	)
)


(define-fun-rec mem ((e elt) (l eltlist)) Bool 
	(
		match l
		(
			(nil false)
			((cons h t) (ite (= e h) true (mem e t)))
		)
	)
)

(assert (forall ((e elt) (l1 eltlist))
			(=> (mem e l1)
				(mem e (reverse l1)))))


(check-sat)