(structure (List-Of T)
  nil
  (cons T (List-Of T)))

(declare append ((T) -> ((List-Of T) (List-Of T)) (List-Of T)))
(define append-axiom1
  (forall ?l
    (= (append nil ?l) ?l)))
(define append-axiom2
  (forall ?x ?rest ?l
    (= (append (cons ?x ?rest) ?l) (cons ?x (append ?rest ?l)))))
(assert append-axiom1 append-axiom2)
     
(declare list-elem ((T) -> (T (List-Of T)) Boolean))
(define list-elem-axiom1
  (forall ?e
    (not (list-elem ?e nil))))
(define list-elem-axiom2
  (forall ?e ?e' ?rest
    (iff (list-elem ?e (cons ?e' ?rest))
         (or (= ?e ?e')
             (list-elem ?e ?rest)))))
(assert list-elem-axiom1 list-elem-axiom2)

(declare list-inter ((T) -> ((List-Of T) (List-Of T)) (List-Of T)))
(define list-inter-axiom
  (forall ?e ?l1 ?l2
    (iff (list-elem ?e (list-inter ?l1 ?l2))
         (and (list-elem ?e ?l1)
              (list-elem ?e ?l2)))))
(assert list-inter-axiom)

(declare prefix ((T) -> ((List-Of T) (List-Of T)) Boolean))

(define prefix-axiom-1
  (forall ?l
    (prefix nil ?l))) 

(define prefix-axiom-2
  (forall ?x ?tail1 ?tail2
    (if (prefix ?tail1 ?tail2)
        (prefix (cons ?x ?tail1) (cons ?x ?tail2)))))

(assert prefix-axiom-1 prefix-axiom-2)