DEFINITION clear_gen_sort()
TYPE =
       ∀x:C.∀n:nat.(clear (CSort n) x)→∀P:Prop.P
BODY =
        assume x: C
        assume n: nat
        suppose H: clear (CSort n) x
        assume P: Prop
           assume y: C
           suppose H0: clear y x
             we proceed by induction on H0 to prove (eq C y (CSort n))→P
                case clear_bind : b:B e:C u:T ⇒
                   the thesis becomes ∀H1:(eq C (CHead e (Bind b) u) (CSort n)).P
                      suppose H1: eq C (CHead e (Bind b) u) (CSort n)
                         (H2) 
                            we proceed by induction on H1 to prove <λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                               case refl_equal : ⇒
                                  the thesis becomes 
                                  <λ:C.Prop> CASE CHead e (Bind b) u OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True

                                        <λ:C.Prop> CASE CHead e (Bind b) u OF CSort ⇒False | CHead   ⇒True
<λ:C.Prop> CASE CSort n OF CSort ⇒False | CHead   ⇒True
                         end of H2
                         consider H2
                         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
∀H1:(eq C (CHead e (Bind b) u) (CSort n)).P
                case clear_flat : e:C c:C :clear e c f:F u:T ⇒
                   the thesis becomes ∀H3:(eq C (CHead e (Flat f) u) (CSort n)).P
                   () by induction hypothesis we know (eq C e (CSort n))→P
                      suppose H3: eq C (CHead e (Flat f) 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 e (Flat f) u OF CSort ⇒False | CHead   ⇒True
                                     consider I
                                     we proved True

                                        <λ:C.Prop> CASE CHead e (Flat f) 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 e (Flat f) u) (CSort n)).P
             we proved (eq C y (CSort n))→P
          we proved ∀y:C.(clear y x)→(eq C y (CSort n))→P
          by (insert_eq . . . . previous H)
          we proved P
       we proved ∀x:C.∀n:nat.(clear (CSort n) x)→∀P:Prop.P