lista konkat w z3

Czy istnieje sposób na połączenie dwóch list w z3? Podobny do operatora @ w ML? Myślałem o zdefiniowaniu go osobiście, ale nie sądzę, że z3 obsługuje rekurencyjne definicje funkcji, tj.

define-fun concat ( (List l1) (List l2) List 
   (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) )
)