;; 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_bug ((l1 eltlist) (l2 eltlist)) eltlist 
	(
		match l1
		(
			(nil nil)
			((cons h1 t1) (cons h1 (append_bug t1 l2)))
		)
	)
)

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

(define-fun-rec member ((e elt) (l1 eltlist)) Bool 
	(
		match l1
		(
			(nil false)
			((cons h1 t1) (ite (= e h1) true (member e t1)))
		)
	)
)


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



(check-sat)