(csequence_map_composition
 (map_composition 0
  (map_composition-1 nil 3513552853
   ("" (skolem!)
    (("" (lemma "coinduction[T3]")
      ((""
        (inst -
         "LAMBDA (cseq1, cseq2: csequence[T3]): EXISTS (cseq: csequence[T1]): map[T2, T3](f23!1)(map[T1, T2](f12!1)(cseq)) = cseq1 AND map[T1, T3](f23!1 o f12!1)(cseq) = cseq2"
         "map[T2, T3](f23!1)(map[T1, T2](f12!1)(cseq!1))"
         "map[T1, T3](f23!1 o f12!1)(cseq!1)")
        (("1" (assert) (("1" (inst + "cseq!1") nil nil)) nil)
         ("2" (delete 2)
          (("2" (expand "bisimulation?")
            (("2" (skosimp*)
              (("2" (expand "map" -)
                (("2" (expand "o")
                  (("2" (smash)
                    (("1" (inst + "rest(cseq!2)")
                      (("1" (decompose-equality)
                        (("1" (decompose-equality -3)
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (decompose-equality)
                      (("2" (decompose-equality -3)
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T3 formal-type-decl nil csequence_map_composition nil)
    (coinduction formula-decl nil csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (bisimulation? adt-def-decl "boolean" csequence_codt nil)
    (T1 formal-type-decl nil csequence_map_composition nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T2 formal-type-decl nil csequence_map_composition nil)
    (map adt-def-decl "csequence[T1]" csequence_codt_map nil)
    (f23!1 skolem-const-decl "[T2 -> T3]" csequence_map_composition
     nil)
    (f12!1 skolem-const-decl "[T1 -> T2]" csequence_map_composition
     nil)
    (O const-decl "T3" function_props nil))
   shostak)))