DEFINITION csubst0_gen_sort()
TYPE =
       ∀x:C.∀v:T.∀i:nat.∀n:nat.(csubst0 i v (CSort n) x)→∀P:Prop.P
BODY =
        assume x: C
        assume v: T
        assume i: nat
        assume n: nat
        suppose H: csubst0 i v (CSort n) x
        assume P: Prop
           assume y: C
           suppose H0: csubst0 i v y x
             we proceed by induction on H0 to prove (eq C y (CSort n))→P
                case csubst0_snd : k:K i0:nat v0:T u1:T u2:T :subst0 i0 v0 u1 u2 c:C ⇒
                   the thesis becomes ∀H2:(eq C (CHead c k u1) (CSort n)).P
                      suppose H2: eq C (CHead c k u1) (CSort n)
                         (H3) 
                            we proceed by induction on H2 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:C.Prop> CASE CHead c k u1 OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True
<λ:C.Prop> CASE CHead c k u1 OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         end of H3
                         consider H3
                         we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove P
                         we proved P
∀H2:(eq C (CHead c k u1) (CSort n)).P
                case csubst0_fst : k:K i0:nat c1:C c2:C v0:T :csubst0 i0 v0 c1 c2 u:T ⇒
                   the thesis becomes ∀H3:(eq C (CHead c1 k u) (CSort n)).P
                   () by induction hypothesis we know (eq C c1 (CSort n))→P
                      suppose H3: eq C (CHead c1 k u) (CSort n)
                         (H4) 
                            we proceed by induction on H3 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:C.Prop> CASE CHead c1 k u OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True
<λ:C.Prop> CASE CHead c1 k u OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         end of H4
                         consider H4
                         we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove P
                         we proved P
∀H3:(eq C (CHead c1 k u) (CSort n)).P
                case csubst0_both : k:K i0:nat v0:T u1:T u2:T :subst0 i0 v0 u1 u2 c1:C c2:C :csubst0 i0 v0 c1 c2 ⇒
                   the thesis becomes ∀H4:(eq C (CHead c1 k u1) (CSort n)).P
                   () by induction hypothesis we know (eq C c1 (CSort n))→P
                      suppose H4: eq C (CHead c1 k u1) (CSort n)
                         (H5) 
                            we proceed by induction on H4 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:C.Prop> CASE CHead c1 k u1 OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True
<λ:C.Prop> CASE CHead c1 k u1 OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         end of H5
                         consider H5
                         we proved <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove P
                         we proved P
∀H4:(eq C (CHead c1 k u1) (CSort n)).P
             we proved (eq C y (CSort n))→P
          we proved ∀y:C.(csubst0 i v y x)→(eq C y (CSort n))→P
          by (insert_eq . . . . previous H)
          we proved P
       we proved ∀x:C.∀v:T.∀i:nat.∀n:nat.(csubst0 i v (CSort n) x)→∀P:Prop.P