type error in induction

[c-cube]

on:

(declare-datatypes () ((List (nil) (cons (head Int) (tail List)))))

(define-fun-rec append
  ((l1 List) (l2 List)) List
  (match l1
         (case nil l2)
         (case (cons hd tl) (cons hd (append tl l2)))))

(define-fun-rec mem
  ((x Int) (l List)) Bool
  (match l
         (case nil false)
         (case (cons hd tl)
           (or (= x hd) (mem x tl)))))

(define-fun-rec subset
  ((l1 List) (l2 List)) Bool
  (match l1
         (case nil true)
         (case (cons hd tl)
           (and (mem hd l2) (subset tl l2)))))

;; subset_cons
(assert (forall ((a Int) (l1 List) (l2 List))
                (=> (subset l1 l2) (subset l1 (cons a l2)))))

;; subset-append
(assert-not (forall ((l1 List) (l2 List) (l3 List))
                    (= (subset (append l1 l2) l3)
                       (and (subset l1 l3) (subset l2 l3)))))
(check-sat)

type error (in Monome).