# TODO

## Proper Encoding of DataTypes

```
(declare-datatypes (T) ((LL lnil (lcons (lhd T) (ltl LL)))))
(declare-fun l1 () (LL Int))
(declare-fun l2 () (LL Int))
(declare-fun l3 () (LL Int))
(declare-fun x  () Int)
(declare-fun zzz () Int)

(assert (not (= l1 (as lnil (LL Int)))))
(assert (not (= l2 (as lnil (LL Int)))))

(assert (= (lhd l1) (lhd l2)))
(assert (not (= l1 l2)))
(assert (= l3 (lcons x l2)))
(assert (> x 100))
(check-sat)

(get-model)


(declare-fun xs () (LL Int))
(declare-fun ys () (LL Int))
(declare-fun y  () Int)

(assert (= xs (as lnil (LL Int))))
(assert (= ys (lcons y ys)))
(assert (= xs ys))
(check-sat)


;; (assert (= (ltl l1) (ltl l2)))
;; (check-sat)
```