DEFINITION ex1_arity()
TYPE =
       ∀g:G.(arity g ex1_c ex1_t (ASort O O))
BODY =
       assume g: G
          (h1) 
             (h1) 
                by (getl_refl . . .)

                   getl
                     O
                     CHead
                       CHead
                         CHead (CSort O) (Bind Abst) (TSort O)
                         Bind Abst
                         TSort O
                       Bind Abst
                       TLRef O
                     CHead
                       CHead
                         CHead (CSort O) (Bind Abst) (TSort O)
                         Bind Abst
                         TSort O
                       Bind Abst
                       TLRef O
             end of h1
             (h2) 
                (h1) 
                   by (getl_refl . . .)

                      getl
                        O
                        CHead
                          CHead (CSort O) (Bind Abst) (TSort O)
                          Bind Abst
                          TSort O
                        CHead
                          CHead (CSort O) (Bind Abst) (TSort O)
                          Bind Abst
                          TSort O
                end of h1
                (h2) 
                   (h1) 
                      by (arity_sort . . .)

                         arity
                           g
                           CHead (CSort O) (Bind Abst) (TSort O)
                           TSort O
                           ASort O O
                   end of h1
                   (h2) 
                      by (ex1__leq_sort_SS . . .)
leq g (ASort O O) (asucc g (asucc g (ASort (S (S O)) O)))
                   end of h2
                   by (arity_repl . . . . h1 . h2)

                      arity
                        g
                        CHead (CSort O) (Bind Abst) (TSort O)
                        TSort O
                        asucc g (asucc g (ASort (S (S O)) O))
                end of h2
                by (arity_abst . . . . . h1 . h2)

                   arity
                     g
                     CHead
                       CHead (CSort O) (Bind Abst) (TSort O)
                       Bind Abst
                       TSort O
                     TLRef O
                     asucc g (ASort (S (S O)) O)
             end of h2
             by (arity_abst . . . . . h1 . h2)

                arity
                  g
                  CHead
                    CHead
                      CHead (CSort O) (Bind Abst) (TSort O)
                      Bind Abst
                      TSort O
                    Bind Abst
                    TLRef O
                  TLRef O
                  ASort (S (S O)) O
          end of h1
          (h2) 
             (h1) 
                (h1) 
                   (h1) 
                      by (clear_bind . . .)

                         clear
                           CHead
                             CHead
                               CHead (CSort O) (Bind Abst) (TSort O)
                               Bind Abst
                               TSort O
                             Bind Abst
                             TLRef O
                           CHead
                             CHead
                               CHead (CSort O) (Bind Abst) (TSort O)
                               Bind Abst
                               TSort O
                             Bind Abst
                             TLRef O
                   end of h1
                   (h2) 
                      by (getl_refl . . .)
                      we proved 
                         getl
                           O
                           CHead (CSort O) (Bind Abst) (TSort O)
                           CHead (CSort O) (Bind Abst) (TSort O)
                      that is equivalent to 
                         getl
                           r (Bind Abst) O
                           CHead (CSort O) (Bind Abst) (TSort O)
                           CHead (CSort O) (Bind Abst) (TSort O)
                      by (getl_head . . . . previous .)

                         getl
                           S O
                           CHead
                             CHead (CSort O) (Bind Abst) (TSort O)
                             Bind Abst
                             TSort O
                           CHead (CSort O) (Bind Abst) (TSort O)
                   end of h2
                   by (getl_clear_bind . . . . h1 . . h2)

                      getl
                        S (S O)
                        CHead
                          CHead
                            CHead (CSort O) (Bind Abst) (TSort O)
                            Bind Abst
                            TSort O
                          Bind Abst
                          TLRef O
                        CHead (CSort O) (Bind Abst) (TSort O)
                end of h1
                (h2) 
                   (h1) 
                      by (arity_sort . . .)
arity g (CSort O) (TSort O) (ASort O O)
                   end of h1
                   (h2) 
                      by (ex1__leq_sort_SS . . .)
leq g (ASort O O) (asucc g (asucc g (ASort (S (S O)) O)))
                   end of h2
                   by (arity_repl . . . . h1 . h2)

                      arity
                        g
                        CSort O
                        TSort O
                        asucc g (asucc g (ASort (S (S O)) O))
                end of h2
                by (arity_abst . . . . . h1 . h2)

                   arity
                     g
                     CHead
                       CHead
                         CHead (CSort O) (Bind Abst) (TSort O)
                         Bind Abst
                         TSort O
                       Bind Abst
                       TLRef O
                     TLRef (S (S O))
                     asucc g (ASort (S (S O)) O)
             end of h1
             (h2) 
                by (arity_sort . . .)

                   arity
                     g
                     CHead
                       CHead
                         CHead
                           CHead (CSort O) (Bind Abst) (TSort O)
                           Bind Abst
                           TSort O
                         Bind Abst
                         TLRef O
                       Bind Abst
                       TLRef (S (S O))
                     TSort O
                     ASort O O
             end of h2
             by (arity_head . . . . h1 . . h2)

                arity
                  g
                  CHead
                    CHead
                      CHead (CSort O) (Bind Abst) (TSort O)
                      Bind Abst
                      TSort O
                    Bind Abst
                    TLRef O
                  THead (Bind Abst) (TLRef (S (S O))) (TSort O)
                  AHead (ASort (S (S O)) O) (ASort O O)
          end of h2
          by (arity_appl . . . . h1 . . h2)
          we proved 
             arity
               g
               CHead
                 CHead
                   CHead (CSort O) (Bind Abst) (TSort O)
                   Bind Abst
                   TSort O
                 Bind Abst
                 TLRef O
               THead
                 Flat Appl
                 TLRef O
                 THead (Bind Abst) (TLRef (S (S O))) (TSort O)
               ASort O O
          that is equivalent to arity g ex1_c ex1_t (ASort O O)
       we proved ∀g:G.(arity g ex1_c ex1_t (ASort O O))