(|caret_arrays| (|caret_TCC1| "" (SUBTYPE-TCC) NIL) (|caret_TCC2| "" (SAME-NAME-TCC) NIL)
 (|caret_TCC3| "" (SUBTYPE-TCC) NIL) (|caret_TCC4| "" (SAME-NAME-TCC) NIL)
 (|caret_TCC5| "" (SUBTYPE-TCC) NIL) (|caret_TCC6| "" (SUBTYPE-TCC) NIL)
 (|caret_TCC7| "" (SUBTYPE-TCC) NIL) (|caret_all_TCC1| "" (SUBTYPE-TCC) NIL)
 (|caret_all_TCC2| "" (SUBTYPE-TCC) NIL)
 (|caret_all| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
    (("1" (GRIND) NIL)
     ("2" (SKOSIMP*)
      (("2" (ASSERT) (("2" (TYPEPRED "y1!1") (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))
 (|caret_ii_0_TCC1| "" (SUBTYPE-TCC) NIL) (|caret_ii_0| "" (SKOSIMP*) (("" (GRIND) NIL)))
 (|caret_elim_TCC1| "" (SUBTYPE-TCC)) (|caret_elim_TCC2| "" (SUBTYPE-TCC) NIL)
 (|caret_elim_TCC3| "" (SUBTYPE-TCC) NIL) (|caret_elim| "" (SKOSIMP*) (("" (GRIND) NIL))))(|empty_array_def|
                                                                                           (|empty_array_TCC1|
                                                                                            ""
                                                                                            (INST
                                                                                             1
                                                                                             " (LAMBDA (x: below[0]): epsilon! (t:T): true)")
                                                                                            ((""
                                                                                              (SKOSIMP*)
                                                                                              NIL))))