DEFINITION wf3_gen_sort1()
TYPE =
       ∀g:G.∀x:C.∀m:nat.(wf3 g (CSort m) x)→(eq C x (CSort m))
BODY =
        assume g: G
        assume x: C
        assume m: nat
        suppose H: wf3 g (CSort m) x
           assume y: C
           suppose H0: wf3 g y x
             we proceed by induction on H0 to prove (eq C y (CSort m))→(eq C x y)
                case wf3_sort : m0:nat ⇒
                   the thesis becomes ∀H1:(eq C (CSort m0) (CSort m)).(eq C (CSort m0) (CSort m0))
                      suppose H1: eq C (CSort m0) (CSort m)
                         (H2) 
                            by (f_equal . . . . . H1)
                            we proved 
                               eq
                                 nat
                                 <λ:C.nat> CASE CSort m0 OF CSort n⇒n | CHead   ⇒m0
                                 <λ:C.nat> CASE CSort m OF CSort n⇒n | CHead   ⇒m0

                               eq
                                 nat
                                 λe:C.<λ:C.nat> CASE e OF CSort n⇒n | CHead   ⇒m0 (CSort m0)
                                 λe:C.<λ:C.nat> CASE e OF CSort n⇒n | CHead   ⇒m0 (CSort m)
                         end of H2
                         (h1) 
                            by (refl_equal . .)
eq C (CSort m) (CSort m)
                         end of h1
                         (h2) 
                            consider H2
                            we proved 
                               eq
                                 nat
                                 <λ:C.nat> CASE CSort m0 OF CSort n⇒n | CHead   ⇒m0
                                 <λ:C.nat> CASE CSort m OF CSort n⇒n | CHead   ⇒m0
eq nat m0 m
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
                         we proved eq C (CSort m0) (CSort m0)
∀H1:(eq C (CSort m0) (CSort m)).(eq C (CSort m0) (CSort m0))
                case wf3_bind : c1:C c2:C :wf3 g c1 c2 u:T t:T :ty3 g c1 u t b:B ⇒
                   the thesis becomes 
                   ∀H4:eq C (CHead c1 (Bind b) u) (CSort m)
                     .eq C (CHead c2 (Bind b) u) (CHead c1 (Bind b) u)
                   () by induction hypothesis we know (eq C c1 (CSort m))→(eq C c2 c1)
                      suppose H4: eq C (CHead c1 (Bind b) u) (CSort m)
                         (H5) 
                            we proceed by induction on H4 to prove <λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:C.Prop> CASE CHead c1 (Bind b) u OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True
<λ:C.Prop> CASE CHead c1 (Bind b) u OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                         end of H5
                         consider H5
                         we proved <λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove eq C (CHead c2 (Bind b) u) (CHead c1 (Bind b) u)
                         we proved eq C (CHead c2 (Bind b) u) (CHead c1 (Bind b) u)

                         ∀H4:eq C (CHead c1 (Bind b) u) (CSort m)
                           .eq C (CHead c2 (Bind b) u) (CHead c1 (Bind b) u)
                case wf3_void : c1:C c2:C :wf3 g c1 c2 u:T :∀t:T.(ty3 g c1 u t)→False b:B ⇒
                   the thesis becomes 
                   ∀H4:eq C (CHead c1 (Bind b) u) (CSort m)
                     .eq C (CHead c2 (Bind Void) (TSort O)) (CHead c1 (Bind b) u)
                   () by induction hypothesis we know (eq C c1 (CSort m))→(eq C c2 c1)
                      suppose H4: eq C (CHead c1 (Bind b) u) (CSort m)
                         (H5) 
                            we proceed by induction on H4 to prove <λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:C.Prop> CASE CHead c1 (Bind b) u OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True
<λ:C.Prop> CASE CHead c1 (Bind b) u OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                         end of H5
                         consider H5
                         we proved <λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove eq C (CHead c2 (Bind Void) (TSort O)) (CHead c1 (Bind b) u)
                         we proved eq C (CHead c2 (Bind Void) (TSort O)) (CHead c1 (Bind b) u)

                         ∀H4:eq C (CHead c1 (Bind b) u) (CSort m)
                           .eq C (CHead c2 (Bind Void) (TSort O)) (CHead c1 (Bind b) u)
                case wf3_flat : c1:C c2:C :wf3 g c1 c2 u:T f:F ⇒
                   the thesis becomes 
                   ∀H3:(eq C (CHead c1 (Flat f) u) (CSort m)).(eq C c2 (CHead c1 (Flat f) u))
                   () by induction hypothesis we know (eq C c1 (CSort m))→(eq C c2 c1)
                      suppose H3: eq C (CHead c1 (Flat f) u) (CSort m)
                         (H4) 
                            we proceed by induction on H3 to prove <λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes <λ:C.Prop> CASE CHead c1 (Flat f) u OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True
<λ:C.Prop> CASE CHead c1 (Flat f) u OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                         end of H4
                         consider H4
                         we proved <λ:C.Prop> CASE CSort m OF CSort ⇒False | CHead   ⇒True
                         that is equivalent to False
                         we proceed by induction on the previous result to prove eq C c2 (CHead c1 (Flat f) u)
                         we proved eq C c2 (CHead c1 (Flat f) u)

                         ∀H3:(eq C (CHead c1 (Flat f) u) (CSort m)).(eq C c2 (CHead c1 (Flat f) u))
             we proved (eq C y (CSort m))→(eq C x y)
          we proved ∀y:C.(wf3 g y x)→(eq C y (CSort m))→(eq C x y)
          by (insert_eq . . . . previous H)
          we proved eq C x (CSort m)
       we proved ∀g:G.∀x:C.∀m:nat.(wf3 g (CSort m) x)→(eq C x (CSort m))