;; Conversion ite échoue
(set-logic HORN)


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

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

(assert (forall ((i elt)(l1 eltlist)(l2 eltlist))
			(=> (and (memberl i l1) (= l1 l2))
				(memberl i l2))))


(check-sat)