DEFINITION clear_gen_flat_r()
TYPE =
       ∀f:F.∀x:C.∀e:C.∀u:T.(clear x (CHead e (Flat f) u))→∀P:Prop.P
BODY =
        assume f: F
        assume x: C
        assume e: C
        assume u: T
        suppose H: clear x (CHead e (Flat f) u)
        assume P: Prop
           assume y: C
           suppose H0: clear x y
             we proceed by induction on H0 to prove (eq C y (CHead e (Flat f) u))→P
                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)).P
                      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 P
                         we proved P
∀H1:(eq C (CHead e0 (Bind b) u0) (CHead e (Flat f) u)).P
                case clear_flat : e0:C c:C H1:clear e0 c :F :T ⇒
                   the thesis becomes ∀H3:(eq C c (CHead e (Flat f) u)).P
                   (H2) by induction hypothesis we know (eq C c (CHead e (Flat f) u))→P
                      suppose H3: eq C c (CHead e (Flat f) u)
                         (H4) 
                            we proceed by induction on H3 to prove (eq C (CHead e (Flat f) u) (CHead e (Flat f) u))→P
                               case refl_equal : ⇒
                                  the thesis becomes the hypothesis H2
(eq C (CHead e (Flat f) u) (CHead e (Flat f) u))→P
                         end of H4
                         by (refl_equal . .)
                         we proved eq C (CHead e (Flat f) u) (CHead e (Flat f) u)
                         by (H4 previous)
                         we proved P
∀H3:(eq C c (CHead e (Flat f) u)).P
             we proved (eq C y (CHead e (Flat f) u))→P
          we proved ∀y:C.(clear x y)→(eq C y (CHead e (Flat f) u))→P
          by (insert_eq . . . . previous H)
          we proved P
       we proved ∀f:F.∀x:C.∀e:C.∀u:T.(clear x (CHead e (Flat f) u))→∀P:Prop.P