DEFINITION aprem_gen_sort()
TYPE =
       ∀x:A.∀i:nat.∀h:nat.∀n:nat.(aprem i (ASort h n) x)→False
BODY =
        assume x: A
        assume i: nat
        assume h: nat
        assume n: nat
        suppose H: aprem i (ASort h n) x
           assume y: A
           suppose H0: aprem i y x
             we proceed by induction on H0 to prove (eq A y (ASort h n))→False
                case aprem_zero : a1:A a2:A ⇒
                   the thesis becomes ∀H1:(eq A (AHead a1 a2) (ASort h n)).False
                      suppose H1: eq A (AHead a1 a2) (ASort h n)
                         (H2) 
                            we proceed by induction on H1 to prove <λ:A.Prop> CASE ASort h n OF ASort  ⇒False | AHead  ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:A.Prop> CASE AHead a1 a2 OF ASort  ⇒False | AHead  ⇒True
                                     consider I
                                     we proved True
<λ:A.Prop> CASE AHead a1 a2 OF ASort  ⇒False | AHead  ⇒True
<λ:A.Prop> CASE ASort h n OF ASort  ⇒False | AHead  ⇒True
                         end of H2
                         consider H2
                         we proved <λ:A.Prop> CASE ASort h n OF ASort  ⇒False | AHead  ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove False
                         we proved False
∀H1:(eq A (AHead a1 a2) (ASort h n)).False
                case aprem_succ : a2:A a:A i0:nat :aprem i0 a2 a a1:A ⇒
                   the thesis becomes ∀H3:(eq A (AHead a1 a2) (ASort h n)).False
                   () by induction hypothesis we know (eq A a2 (ASort h n))→False
                      suppose H3: eq A (AHead a1 a2) (ASort h n)
                         (H4) 
                            we proceed by induction on H3 to prove <λ:A.Prop> CASE ASort h n OF ASort  ⇒False | AHead  ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:A.Prop> CASE AHead a1 a2 OF ASort  ⇒False | AHead  ⇒True
                                     consider I
                                     we proved True
<λ:A.Prop> CASE AHead a1 a2 OF ASort  ⇒False | AHead  ⇒True
<λ:A.Prop> CASE ASort h n OF ASort  ⇒False | AHead  ⇒True
                         end of H4
                         consider H4
                         we proved <λ:A.Prop> CASE ASort h n OF ASort  ⇒False | AHead  ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove False
                         we proved False
∀H3:(eq A (AHead a1 a2) (ASort h n)).False
             we proved (eq A y (ASort h n))→False
          we proved ∀y:A.(aprem i y x)→(eq A y (ASort h n))→False
          by (insert_eq . . . . previous H)
          we proved False
       we proved ∀x:A.∀i:nat.∀h:nat.∀n:nat.(aprem i (ASort h n) x)→False