(|th_Gb| (H_TCC1 "" (EXISTENCE-TCC))
 (L1 "" (SKOLEM 1 "A")
  (("" (TYPEPRED "A") (("" (FLATTEN) (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (L2 "" (ASSERT)
  (("" (LEMMA "L1")
    (("" (INST-CP -1 "H(a)")
      (("" (INST-CP -1 "H(b)")
        (("" (INST -1 "H(c)")
          (("" (TYPEPRED "H")
            (("" (SPLIT)
              (("1" (SPLIT)
                (("1" (SPLIT)
                  (("1" (INST?)
                    (("1" (INST?)
                      (("1" (LEMMA "PPL_disjoint")
                        (("1" (TYPEPRED "H")
                          (("1" (INST -1 "a" "b")
                            (("1" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (INST -4 "b" "c") (("2" (ASSERT) NIL NIL)) NIL)
                   ("3" (INST -4 "b" "c") (("3" (ASSERT) NIL NIL))
                    NIL))
                  NIL)
                 ("2" (INST? 1) NIL NIL) ("3" (INST? 1) NIL NIL))
                NIL)
               ("2" (SPLIT)
                (("1" (INST? 1) NIL NIL)
                 ("2" (INST? -3)
                  (("2" (INST -3 "c") (("2" (ASSERT) NIL NIL)) NIL))
                  NIL)
                 ("3" (SPLIT)
                  (("1" (INST? 1) NIL NIL)
                   ("2" (INST -4 "a" "c") (("2" (ASSERT) NIL NIL)) NIL)
                   ("3" (INST -4 "a" "b") (("3" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL)
               ("3" (SPLIT)
                (("1" (INST 1 "b") NIL NIL)
                 ("2" (SPLIT)
                  (("1" (INST 1 "a") NIL NIL)
                   ("2" (INST -4 "a" "b") (("2" (ASSERT) NIL NIL)) NIL)
                   ("3" (INST -4 "a" "c") (("3" (ASSERT) NIL NIL))
                    NIL))
                  NIL)
                 ("3" (SPLIT)
                  (("1" (INST 1 "a") NIL NIL)
                   ("2" (INST -4 "b" "c") (("2" (ASSERT) NIL NIL)) NIL)
                   ("3" (INST -4 "a" "b")
                    (("3" (SPLIT)
                      (("1" (LEMMA "PPL_disjoint")
                        (("1" (INST?)
                          (("1" (FLATTEN) (("1" (ASSERT) NIL NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (ASSERT) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))