(set-logic ALL) ; has lambda expressions, using catch-all.
(declare-sort A 0)  ; N.B. Uninterpreted sort.
(declare-fun A_witness () A)
(declare-sort B 0)  ; N.B. Uninterpreted sort.
(declare-fun B_witness () B)
(declare-fun f (A) B)
(define-fun-rec sbv.map_532386 ((lst (Seq A))) (Seq B)
              (ite (= lst (as seq.empty (Seq A)))
                   (as seq.empty (Seq B))
                   (seq.++ (seq.unit (select (lambda ((l2_s0 A))
  (f l2_s0)) (seq.nth lst 0)))
                           (sbv.map_532386 (seq.extract lst 1 (- (seq.len lst) 1))))))
(define-fun-rec sbv.reverse_3f0381 ((lst (Seq B))) (Seq B)
                (ite (= lst (as seq.empty (Seq B)))
                     (as seq.empty (Seq B))
                     (seq.++ (sbv.reverse_3f0381 (seq.extract lst 1 (- (seq.len lst) 1))) (seq.unit (seq.nth lst 0)))))
(define-fun-rec sbv.reverse_8fc8f1 ((lst (Seq A))) (Seq A)
                (ite (= lst (as seq.empty (Seq A)))
                     (as seq.empty (Seq A))
                     (seq.++ (sbv.reverse_8fc8f1 (seq.extract lst 1 (- (seq.len lst) 1))) (seq.unit (seq.nth lst 0)))))
(define-fun s0 () Bool (forall ((l1_s0 A) (l1_s1 (Seq A)))
                          (let ((l1_s2 (f l1_s0)))
                          (let ((l1_s3 (seq.unit l1_s2)))
                          (let ((l1_s4 (sbv.map_532386 l1_s1)))
                          (let ((l1_s5 (seq.++ l1_s3 l1_s4)))
                          (let ((l1_s6 (sbv.reverse_3f0381 l1_s5)))
                          (let ((l1_s7 (sbv.reverse_3f0381 l1_s4)))
                          (let ((l1_s8 (seq.++ l1_s7 l1_s3)))
                          (let ((l1_s9 (= l1_s6 l1_s8)))
                          l1_s9))))))))))
(define-fun s1 () Bool s0) ; mapReverse.2
(define-fun s2 () Bool (forall ((l1_s0 A) (l1_s1 (Seq A)))
                          (let ((l1_s2 (seq.unit l1_s0)))
                          (let ((l1_s3 (seq.++ l1_s2 l1_s1)))
                          (let ((l1_s4 (sbv.map_532386 l1_s3)))
                          (let ((l1_s5 (sbv.reverse_3f0381 l1_s4)))
                          (let ((l1_s6 (f l1_s0)))
                          (let ((l1_s7 (seq.unit l1_s6)))
                          (let ((l1_s8 (sbv.map_532386 l1_s1)))
                          (let ((l1_s9 (seq.++ l1_s7 l1_s8)))
                          (let ((l1_s10 (sbv.reverse_3f0381 l1_s9)))
                          (let ((l1_s11 (= l1_s5 l1_s10)))
                          l1_s11))))))))))))
(define-fun s3 () Bool s2) ; mapReverse.1
(define-fun s4 () Bool (forall ((l1_s0 A) (l1_s1 (Seq A)))
                          (let ((l1_s2 (sbv.map_532386 l1_s1)))
                          (let ((l1_s3 (sbv.reverse_3f0381 l1_s2)))
                          (let ((l1_s4 (sbv.reverse_8fc8f1 l1_s1)))
                          (let ((l1_s5 (sbv.map_532386 l1_s4)))
                          (let ((l1_s6 (= l1_s3 l1_s5)))
                          (let ((l1_s7 (seq.unit l1_s0)))
                          (let ((l1_s8 (seq.++ l1_s7 l1_s1)))
                          (let ((l1_s9 (sbv.map_532386 l1_s8)))
                          (let ((l1_s10 (sbv.reverse_3f0381 l1_s9)))
                          (let ((l1_s11 (sbv.reverse_8fc8f1 l1_s8)))
                          (let ((l1_s12 (sbv.map_532386 l1_s11)))
                          (let ((l1_s13 (= l1_s10 l1_s12)))
                          (let ((l1_s14 (=> l1_s6 l1_s13)))
                          l1_s14)))))))))))))))
(define-fun s5 () Bool (forall ((l1_s0 (Seq A)))
                          (let ((l1_s1 (sbv.map_532386 l1_s0)))
                          (let ((l1_s2 (sbv.reverse_3f0381 l1_s1)))
                          (let ((l1_s3 (sbv.reverse_8fc8f1 l1_s0)))
                          (let ((l1_s4 (sbv.map_532386 l1_s3)))
                          (let ((l1_s5 (= l1_s2 l1_s4)))
                          l1_s5)))))))
(define-fun s6 () Bool (=> s4 s5))
(define-fun s7 () Bool s6) ; List(a).induct
(define-fun s8 () Bool (forall ((l1_s0 A) (l1_s1 (Seq A)))
                          (let ((l1_s2 (seq.unit l1_s0)))
                          (let ((l1_s3 (seq.++ l1_s2 l1_s1)))
                          (let ((l1_s4 (sbv.reverse_8fc8f1 l1_s3)))
                          (let ((l1_s5 (sbv.reverse_8fc8f1 l1_s1)))
                          (let ((l1_s6 (seq.++ l1_s5 l1_s2)))
                          (let ((l1_s7 (= l1_s4 l1_s6)))
                          l1_s7))))))))
(define-fun s9 () Bool s8) ; revCons
(define-fun s10 () Bool (forall ((l1_s0 (Seq A)) (l1_s1 (Seq A)))
                          (let ((l1_s2 (seq.++ l1_s0 l1_s1)))
                          (let ((l1_s3 (sbv.map_532386 l1_s2)))
                          (let ((l1_s4 (sbv.map_532386 l1_s0)))
                          (let ((l1_s5 (sbv.map_532386 l1_s1)))
                          (let ((l1_s6 (seq.++ l1_s4 l1_s5)))
                          (let ((l1_s7 (= l1_s3 l1_s6)))
                          l1_s7))))))))
(define-fun s11 () Bool s10) ; mapAppend
(define-fun s12 () Bool (forall ((l1_s0 A) (l1_s1 (Seq A)))
                          (let ((l1_s2 (sbv.map_532386 l1_s1)))
                          (let ((l1_s3 (sbv.reverse_3f0381 l1_s2)))
                          (let ((l1_s4 (f l1_s0)))
                          (let ((l1_s5 (seq.unit l1_s4)))
                          (let ((l1_s6 (seq.++ l1_s3 l1_s5)))
                          (let ((l1_s7 (sbv.reverse_8fc8f1 l1_s1)))
                          (let ((l1_s8 (sbv.map_532386 l1_s7)))
                          (let ((l1_s9 (seq.++ l1_s8 l1_s5)))
                          (let ((l1_s10 (= l1_s6 l1_s9)))
                          l1_s10)))))))))))
(assert s1)
(assert s3)
(assert s7)
(assert s9)
(assert s11)
(assert (not s12))
(check-sat)