DEFINITION asucc_repl()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→(leq g (asucc g a1) (asucc g a2))
BODY =
        assume g: G
        assume a1: A
        assume a2: A
        suppose H: leq g a1 a2
          we proceed by induction on H to prove leq g (asucc g a1) (asucc g a2)
             case leq_sort : h1:nat h2:nat n1:nat n2:nat k:nat H0:eq A (aplus g (ASort h1 n1) k) (aplus g (ASort h2 n2) k) ⇒
                the thesis becomes leq g (asucc g (ASort h1 n1)) (asucc g (ASort h2 n2))
                   suppose H1: eq A (aplus g (ASort O n1) k) (aplus g (ASort h2 n2) k)
                      suppose H2: eq A (aplus g (ASort O n1) k) (aplus g (ASort O n2) k)
                         by (aplus_sort_O_S_simpl . . .)
                         we proved 
                            eq
                              A
                              aplus g (ASort O n1) (S k)
                              aplus g (ASort O (next g n1)) k
                         we proceed by induction on the previous result to prove 
                            eq
                              A
                              aplus g (ASort O (next g n1)) k
                              aplus g (ASort O (next g n2)) k
                            case refl_equal : ⇒
                               the thesis becomes 
                               eq
                                 A
                                 aplus g (ASort O n1) (S k)
                                 aplus g (ASort O (next g n2)) k
                                  by (aplus_sort_O_S_simpl . . .)
                                  we proved 
                                     eq
                                       A
                                       aplus g (ASort O n2) (S k)
                                       aplus g (ASort O (next g n2)) k
                                  we proceed by induction on the previous result to prove 
                                     eq
                                       A
                                       aplus g (ASort O n1) (S k)
                                       aplus g (ASort O (next g n2)) k
                                     case refl_equal : ⇒
                                        the thesis becomes eq A (aplus g (ASort O n1) (S k)) (aplus g (ASort O n2) (S k))
                                           by (refl_equal . .)
                                           we proved 
                                              eq
                                                A
                                                asucc g (aplus g (ASort O n2) k)
                                                asucc g (aplus g (ASort O n2) k)
                                           by (eq_ind_r . . . previous . H2)
                                           we proved 
                                              eq
                                                A
                                                asucc g (aplus g (ASort O n1) k)
                                                asucc g (aplus g (ASort O n2) k)
eq A (aplus g (ASort O n1) (S k)) (aplus g (ASort O n2) (S k))

                                     eq
                                       A
                                       aplus g (ASort O n1) (S k)
                                       aplus g (ASort O (next g n2)) k
                         we proved 
                            eq
                              A
                              aplus g (ASort O (next g n1)) k
                              aplus g (ASort O (next g n2)) k
                         by (leq_sort . . . . . . previous)
                         we proved leq g (ASort O (next g n1)) (ASort O (next g n2))
                         that is equivalent to 
                            leq
                              g
                              ASort O (next g n1)
                              <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2

                         eq A (aplus g (ASort O n1) k) (aplus g (ASort O n2) k)
                           →(leq
                                g
                                ASort O (next g n1)
                                <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                       assume h3: nat
                          suppose : 
                             eq A (aplus g (ASort O n1) k) (aplus g (ASort h3 n2) k)
                               →(leq
                                    g
                                    ASort O (next g n1)
                                    <λn:nat.A> CASE h3 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                         suppose H2: eq A (aplus g (ASort O n1) k) (aplus g (ASort (S h3) n2) k)
                            by (aplus_sort_O_S_simpl . . .)
                            we proved 
                               eq
                                 A
                                 aplus g (ASort O n1) (S k)
                                 aplus g (ASort O (next g n1)) k
                            we proceed by induction on the previous result to prove eq A (aplus g (ASort O (next g n1)) k) (aplus g (ASort h3 n2) k)
                               case refl_equal : ⇒
                                  the thesis becomes eq A (aplus g (ASort O n1) (S k)) (aplus g (ASort h3 n2) k)
                                     by (aplus_sort_S_S_simpl . . . .)
                                     we proved eq A (aplus g (ASort (S h3) n2) (S k)) (aplus g (ASort h3 n2) k)
                                     we proceed by induction on the previous result to prove eq A (aplus g (ASort O n1) (S k)) (aplus g (ASort h3 n2) k)
                                        case refl_equal : ⇒
                                           the thesis becomes 
                                           eq A (aplus g (ASort O n1) (S k)) (aplus g (ASort (S h3) n2) (S k))
                                              by (refl_equal . .)
                                              we proved 
                                                 eq
                                                   A
                                                   asucc g (aplus g (ASort (S h3) n2) k)
                                                   asucc g (aplus g (ASort (S h3) n2) k)
                                              by (eq_ind_r . . . previous . H2)
                                              we proved 
                                                 eq
                                                   A
                                                   asucc g (aplus g (ASort O n1) k)
                                                   asucc g (aplus g (ASort (S h3) n2) k)

                                                 eq A (aplus g (ASort O n1) (S k)) (aplus g (ASort (S h3) n2) (S k))
eq A (aplus g (ASort O n1) (S k)) (aplus g (ASort h3 n2) k)
                            we proved eq A (aplus g (ASort O (next g n1)) k) (aplus g (ASort h3 n2) k)
                            by (leq_sort . . . . . . previous)
                            we proved leq g (ASort O (next g n1)) (ASort h3 n2)
                            that is equivalent to 
                               leq
                                 g
                                 ASort O (next g n1)
                                 <λn3:nat.A> CASE S h3 OF O⇒ASort O (next g n2) | S h⇒ASort h n2

                            ∀H2:eq A (aplus g (ASort O n1) k) (aplus g (ASort (S h3) n2) k)
                              .leq g (ASort O (next g n1)) (ASort h3 n2)
                      by (previous . H1)
                      we proved 
                         leq
                           g
                           ASort O (next g n1)
                           <λn3:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2
                      that is equivalent to 
                         leq
                           g
                           <λn3:nat.A> CASE O OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                           <λn3:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2

                      eq A (aplus g (ASort O n1) k) (aplus g (ASort h2 n2) k)
                        →(leq
                             g
                             <λn3:nat.A> CASE O OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                             <λn3:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                    assume h3: nat
                       suppose IHh1: 
                          eq A (aplus g (ASort h3 n1) k) (aplus g (ASort h2 n2) k)
                            →(leq
                                 g
                                 <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                 <λn:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                      suppose H1: eq A (aplus g (ASort (S h3) n1) k) (aplus g (ASort h2 n2) k)
                         suppose H2: eq A (aplus g (ASort (S h3) n1) k) (aplus g (ASort O n2) k)
                            we must prove 
                                  eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) k)
                                      →(leq
                                           g
                                           <λn3:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                           <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                                    →(leq
                                         g
                                         ASort h3 n1
                                         <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                            or equivalently 
                                  eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) k)
                                      →(leq
                                           g
                                           <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                           ASort O (next g n2))
                                    →(leq
                                         g
                                         ASort h3 n1
                                         <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                            suppose : 
                               eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) k)
                                 →(leq
                                      g
                                      <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                      ASort O (next g n2))
                               by (aplus_sort_O_S_simpl . . .)
                               we proved 
                                  eq
                                    A
                                    aplus g (ASort O n2) (S k)
                                    aplus g (ASort O (next g n2)) k
                               we proceed by induction on the previous result to prove eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O (next g n2)) k)
                                  case refl_equal : ⇒
                                     the thesis becomes eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) (S k))
                                        by (aplus_sort_S_S_simpl . . . .)
                                        we proved eq A (aplus g (ASort (S h3) n1) (S k)) (aplus g (ASort h3 n1) k)
                                        we proceed by induction on the previous result to prove eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) (S k))
                                           case refl_equal : ⇒
                                              the thesis becomes 
                                              eq A (aplus g (ASort (S h3) n1) (S k)) (aplus g (ASort O n2) (S k))
                                                 by (refl_equal . .)
                                                 we proved 
                                                    eq
                                                      A
                                                      asucc g (aplus g (ASort O n2) k)
                                                      asucc g (aplus g (ASort O n2) k)
                                                 by (eq_ind_r . . . previous . H2)
                                                 we proved 
                                                    eq
                                                      A
                                                      asucc g (aplus g (ASort (S h3) n1) k)
                                                      asucc g (aplus g (ASort O n2) k)

                                                    eq A (aplus g (ASort (S h3) n1) (S k)) (aplus g (ASort O n2) (S k))
eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) (S k))
                               we proved eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O (next g n2)) k)
                               by (leq_sort . . . . . . previous)
                               we proved leq g (ASort h3 n1) (ASort O (next g n2))
                               that is equivalent to 
                                  leq
                                    g
                                    ASort h3 n1
                                    <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2
                            we proved 
                               eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) k)
                                   →(leq
                                        g
                                        <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                        ASort O (next g n2))
                                 →(leq
                                      g
                                      ASort h3 n1
                                      <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                            that is equivalent to 
                               eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) k)
                                   →(leq
                                        g
                                        <λn3:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                        <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                                 →(leq
                                      g
                                      ASort h3 n1
                                      <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)

                            eq A (aplus g (ASort (S h3) n1) k) (aplus g (ASort O n2) k)
                              →(eq A (aplus g (ASort h3 n1) k) (aplus g (ASort O n2) k)
                                     →(leq
                                          g
                                          <λn3:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                          <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                                   →(leq
                                        g
                                        ASort h3 n1
                                        <λn3:nat.A> CASE O OF O⇒ASort O (next g n2) | S h⇒ASort h n2))
                          assume h4: nat
                             suppose : 
                                eq A (aplus g (ASort (S h3) n1) k) (aplus g (ASort h4 n2) k)
                                  →(eq A (aplus g (ASort h3 n1) k) (aplus g (ASort h4 n2) k)
                                         →(leq
                                              g
                                              <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                              <λn:nat.A> CASE h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                                       →(leq
                                            g
                                            ASort h3 n1
                                            <λn:nat.A> CASE h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2))
                            suppose H2: eq A (aplus g (ASort (S h3) n1) k) (aplus g (ASort (S h4) n2) k)
                               we must prove 
                                     eq A (aplus g (ASort h3 n1) k) (aplus g (ASort (S h4) n2) k)
                                         →(leq
                                              g
                                              <λn3:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                              <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                                       →(leq
                                            g
                                            ASort h3 n1
                                            <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                               or equivalently 
                                     eq A (aplus g (ASort h3 n1) k) (aplus g (ASort (S h4) n2) k)
                                         →(leq
                                              g
                                              <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                              ASort h4 n2)
                                       →(leq
                                            g
                                            ASort h3 n1
                                            <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                               suppose : 
                                  eq A (aplus g (ASort h3 n1) k) (aplus g (ASort (S h4) n2) k)
                                    →(leq
                                         g
                                         <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                         ASort h4 n2)
                                  by (aplus_sort_S_S_simpl . . . .)
                                  we proved eq A (aplus g (ASort (S h3) n1) (S k)) (aplus g (ASort h3 n1) k)
                                  we proceed by induction on the previous result to prove eq A (aplus g (ASort h3 n1) k) (aplus g (ASort h4 n2) k)
                                     case refl_equal : ⇒
                                        the thesis becomes eq A (aplus g (ASort (S h3) n1) (S k)) (aplus g (ASort h4 n2) k)
                                           by (aplus_sort_S_S_simpl . . . .)
                                           we proved eq A (aplus g (ASort (S h4) n2) (S k)) (aplus g (ASort h4 n2) k)
                                           we proceed by induction on the previous result to prove eq A (aplus g (ASort (S h3) n1) (S k)) (aplus g (ASort h4 n2) k)
                                              case refl_equal : ⇒
                                                 the thesis becomes 
                                                 eq
                                                   A
                                                   aplus g (ASort (S h3) n1) (S k)
                                                   aplus g (ASort (S h4) n2) (S k)
                                                    by (refl_equal . .)
                                                    we proved 
                                                       eq
                                                         A
                                                         asucc g (aplus g (ASort (S h4) n2) k)
                                                         asucc g (aplus g (ASort (S h4) n2) k)
                                                    by (eq_ind_r . . . previous . H2)
                                                    we proved 
                                                       eq
                                                         A
                                                         asucc g (aplus g (ASort (S h3) n1) k)
                                                         asucc g (aplus g (ASort (S h4) n2) k)

                                                       eq
                                                         A
                                                         aplus g (ASort (S h3) n1) (S k)
                                                         aplus g (ASort (S h4) n2) (S k)
eq A (aplus g (ASort (S h3) n1) (S k)) (aplus g (ASort h4 n2) k)
                                  we proved eq A (aplus g (ASort h3 n1) k) (aplus g (ASort h4 n2) k)
                                  by (leq_sort . . . . . . previous)
                                  we proved leq g (ASort h3 n1) (ASort h4 n2)
                                  that is equivalent to 
                                     leq
                                       g
                                       ASort h3 n1
                                       <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2
                               we proved 
                                  eq A (aplus g (ASort h3 n1) k) (aplus g (ASort (S h4) n2) k)
                                      →(leq
                                           g
                                           <λn:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                           ASort h4 n2)
                                    →(leq
                                         g
                                         ASort h3 n1
                                         <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                               that is equivalent to 
                                  eq A (aplus g (ASort h3 n1) k) (aplus g (ASort (S h4) n2) k)
                                      →(leq
                                           g
                                           <λn3:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                           <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                                    →(leq
                                         g
                                         ASort h3 n1
                                         <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)

                               ∀H2:eq A (aplus g (ASort (S h3) n1) k) (aplus g (ASort (S h4) n2) k)
                                 .eq A (aplus g (ASort h3 n1) k) (aplus g (ASort (S h4) n2) k)
                                     →(leq
                                          g
                                          <λn3:nat.A> CASE h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                                          <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                                   →(leq
                                        g
                                        ASort h3 n1
                                        <λn3:nat.A> CASE S h4 OF O⇒ASort O (next g n2) | S h⇒ASort h n2)
                         by (previous . H1 IHh1)
                         we proved 
                            leq
                              g
                              ASort h3 n1
                              <λn3:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2
                         that is equivalent to 
                            leq
                              g
                              <λn3:nat.A> CASE S h3 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                              <λn3:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2

                         ∀H1:eq A (aplus g (ASort (S h3) n1) k) (aplus g (ASort h2 n2) k)
                           .leq
                             g
                             ASort h3 n1
                             <λn3:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2
                   by (previous . H0)
                   we proved 
                      leq
                        g
                        <λn3:nat.A> CASE h1 OF O⇒ASort O (next g n1) | S h⇒ASort h n1
                        <λn3:nat.A> CASE h2 OF O⇒ASort O (next g n2) | S h⇒ASort h n2
leq g (asucc g (ASort h1 n1)) (asucc g (ASort h2 n2))
             case leq_head : a3:A a4:A H0:leq g a3 a4 a5:A a6:A :leq g a5 a6 ⇒
                the thesis becomes leq g (asucc g (AHead a3 a5)) (asucc g (AHead a4 a6))
                () by induction hypothesis we know leq g (asucc g a3) (asucc g a4)
                (H3) by induction hypothesis we know leq g (asucc g a5) (asucc g a6)
                   by (leq_head . . . H0 . . H3)
                   we proved leq g (AHead a3 (asucc g a5)) (AHead a4 (asucc g a6))
leq g (asucc g (AHead a3 a5)) (asucc g (AHead a4 a6))
          we proved leq g (asucc g a1) (asucc g a2)
       we proved ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→(leq g (asucc g a1) (asucc g a2))