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


(declare-datatypes ((nat 0) (natlist 0)) 
	(
		(
			(z) 
			(s (pred nat))
		)
		(
			(nil)
			(cons (hd nat) (tl natlist))
		)
	)
)

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

(assert (forall ((i nat)(l1 natlist)(l2 natlist))
			(=> (and (memberl i l1) (= l1 l2))
				(memberl i l2))))


(check-sat)