;; 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)))
		)
	)
)

(define-fun-rec not_null ((l natlist)) Bool
	(
		match l
		( 
			(nil false)
			( (cons x ll) true)
		)
	)
)

(assert (forall ((i1 nat) (i2 nat)(l natlist))
			(=> (memberl i1 (cons i2 l))
				(memberl i1 l))))


(check-sat)