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

                                        <λ:C.Prop>
                                          CASE CHead e0 (Bind b) u0 OF
                                            CSort ⇒False
                                          | CHead  k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False

                               <λ:C.Prop>
                                 CASE CHead e (Flat f) u OF
                                   CSort ⇒False
                                 | CHead  k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                         end of H2
                         consider H2
                         we proved 
                            <λ:C.Prop>
                              CASE CHead e (Flat f) u OF
                                CSort ⇒False
                              | CHead  k ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                         that is equivalent to False
                         we proceed by induction on the previous result to prove clear e (CHead e0 (Bind b) u0)
                         we proved clear e (CHead e0 (Bind b) u0)

                         ∀H1:eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u)
                           .clear e (CHead e0 (Bind b) u0)
                case clear_flat : e0:C c:C H1:clear e0 c f0:F u0:T ⇒
                   the thesis becomes ∀H3:(eq C (CHead e0 (Flat f0) u0) (CHead e (Flat f) u)).(clear e c)
                   (H2) by induction hypothesis we know (eq C e0 (CHead e (Flat f) u))→(clear e c)
                      suppose H3: eq C (CHead e0 (Flat f0) u0) (CHead e (Flat f) u)
                         (H4) 
                            by (f_equal . . . . . H3)
                            we proved 
                               eq
                                 C
                                 <λ:C.C> CASE CHead e0 (Flat f0) u0 OF CSort ⇒e0 | CHead c0  ⇒c0
                                 <λ:C.C> CASE CHead e (Flat f) u OF CSort ⇒e0 | CHead c0  ⇒c0

                               eq
                                 C
                                 λe1:C.<λ:C.C> CASE e1 OF CSort ⇒e0 | CHead c0  ⇒c0 (CHead e0 (Flat f0) u0)
                                 λe1:C.<λ:C.C> CASE e1 OF CSort ⇒e0 | CHead c0  ⇒c0 (CHead e (Flat f) u)
                         end of H4
                         (h1) 
                            (H5) 
                               by (f_equal . . . . . H3)
                               we proved 
                                  eq
                                    F
                                    <λ:C.F>
                                      CASE CHead e0 (Flat f0) u0 OF
                                        CSort ⇒f0
                                      | CHead  k ⇒<λ:K.F> CASE k OF Bind ⇒f0 | Flat f1⇒f1
                                    <λ:C.F>
                                      CASE CHead e (Flat f) u OF
                                        CSort ⇒f0
                                      | CHead  k ⇒<λ:K.F> CASE k OF Bind ⇒f0 | Flat f1⇒f1

                                  eq
                                    F
                                    λe1:C.<λ:C.F> CASE e1 OF CSort ⇒f0 | CHead  k ⇒<λ:K.F> CASE k OF Bind ⇒f0 | Flat f1⇒f1
                                      CHead e0 (Flat f0) u0
                                    λe1:C.<λ:C.F> CASE e1 OF CSort ⇒f0 | CHead  k ⇒<λ:K.F> CASE k OF Bind ⇒f0 | Flat f1⇒f1
                                      CHead e (Flat f) u
                            end of H5
                            () 
                               consider H5
                               we proved 
                                  eq
                                    F
                                    <λ:C.F>
                                      CASE CHead e0 (Flat f0) u0 OF
                                        CSort ⇒f0
                                      | CHead  k ⇒<λ:K.F> CASE k OF Bind ⇒f0 | Flat f1⇒f1
                                    <λ:C.F>
                                      CASE CHead e (Flat f) u OF
                                        CSort ⇒f0
                                      | CHead  k ⇒<λ:K.F> CASE k OF Bind ⇒f0 | Flat f1⇒f1
eq F f0 f
                            end of 
                            suppose H8: eq C e0 e
                               (H10) 
                                  we proceed by induction on H8 to prove clear e c
                                     case refl_equal : ⇒
                                        the thesis becomes the hypothesis H1
clear e c
                               end of H10
                               consider H10
                               we proved clear e c
(eq C e0 e)→(clear e c)
                         end of h1
                         (h2) 
                            consider H4
                            we proved 
                               eq
                                 C
                                 <λ:C.C> CASE CHead e0 (Flat f0) u0 OF CSort ⇒e0 | CHead c0  ⇒c0
                                 <λ:C.C> CASE CHead e (Flat f) u OF CSort ⇒e0 | CHead c0  ⇒c0
eq C e0 e
                         end of h2
                         by (h1 h2)
                         we proved clear e c
∀H3:(eq C (CHead e0 (Flat f0) u0) (CHead e (Flat f) u)).(clear e c)
             we proved (eq C y (CHead e (Flat f) u))→(clear e x)
          we proved 
             ∀y:C
               .(clear y x)→(eq C y (CHead e (Flat f) u))→(clear e x)
          by (insert_eq . . . . previous H)
          we proved clear e x
       we proved ∀f:F.∀e:C.∀x:C.∀u:T.(clear (CHead e (Flat f) u) x)→(clear e x)