DEFINITION iso_flats_flat_bind_false()
TYPE =
       ∀f1:F
         .∀f2:F
           .∀b:B
             .∀v:T
               .∀v2:T
                 .∀t:T
                   .∀t2:T
                     .∀vs:TList
                       .(iso
                           THeads (Flat f1) vs (THead (Flat f2) v2 t2)
                           THead (Bind b) v t)
                         →∀P:Prop.P
BODY =
        assume f1: F
        assume f2: F
        assume b: B
        assume v: T
        assume v2: T
        assume t: T
        assume t2: T
        assume vs: TList
          we proceed by induction on vs to prove 
             (iso
                 THeads (Flat f1) vs (THead (Flat f2) v2 t2)
                 THead (Bind b) v t)
               →∀P:Prop.P
             case TNil : ⇒
                the thesis becomes 
                (iso
                    THeads (Flat f1) TNil (THead (Flat f2) v2 t2)
                    THead (Bind b) v t)
                  →∀P:Prop.P
                   we must prove 
                         (iso
                             THeads (Flat f1) TNil (THead (Flat f2) v2 t2)
                             THead (Bind b) v t)
                           →∀P:Prop.P
                   or equivalently (iso (THead (Flat f2) v2 t2) (THead (Bind b) v t))→∀P:Prop.P
                    suppose H: iso (THead (Flat f2) v2 t2) (THead (Bind b) v t)
                    assume P: Prop
                      (H_x) 
                         by (iso_gen_head . . . . H)
ex_2 T T λv2:T.λt2:T.eq T (THead (Bind b) v t) (THead (Flat f2) v2 t2)
                      end of H_x
                      (H0) consider H_x
                      we proceed by induction on H0 to prove P
                         case ex_2_intro : x0:T x1:T H1:eq T (THead (Bind b) v t) (THead (Flat f2) x0 x1) ⇒
                            the thesis becomes P
                               (H2) 
                                  we proceed by induction on H1 to prove 
                                     <λ:T.Prop>
                                       CASE THead (Flat f2) x0 x1 OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                                     case refl_equal : ⇒
                                        the thesis becomes 
                                        <λ:T.Prop>
                                          CASE THead (Bind b) v t OF
                                            TSort ⇒False
                                          | TLRef ⇒False
                                          | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                                           consider I
                                           we proved True

                                              <λ:T.Prop>
                                                CASE THead (Bind b) v t OF
                                                  TSort ⇒False
                                                | TLRef ⇒False
                                                | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False

                                     <λ:T.Prop>
                                       CASE THead (Flat f2) x0 x1 OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                               end of H2
                               consider H2
                               we proved 
                                  <λ:T.Prop>
                                    CASE THead (Flat f2) x0 x1 OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead 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
P
                      we proved P
                   we proved (iso (THead (Flat f2) v2 t2) (THead (Bind b) v t))→∀P:Prop.P

                      (iso
                          THeads (Flat f1) TNil (THead (Flat f2) v2 t2)
                          THead (Bind b) v t)
                        →∀P:Prop.P
             case TCons : t0:T t1:TList ⇒
                the thesis becomes 
                (iso
                    THeads (Flat f1) (TCons t0 t1) (THead (Flat f2) v2 t2)
                    THead (Bind b) v t)
                  →∀P:Prop.P
                () by induction hypothesis we know 
                   iso (THeads (Flat f1) t1 (THead (Flat f2) v2 t2)) (THead (Bind b) v t)
                     →∀P:Prop.P
                   we must prove 
                         (iso
                             THeads (Flat f1) (TCons t0 t1) (THead (Flat f2) v2 t2)
                             THead (Bind b) v t)
                           →∀P:Prop.P
                   or equivalently 
                         (iso
                             THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))
                             THead (Bind b) v t)
                           →∀P:Prop.P
                    suppose H0: 
                       iso
                         THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))
                         THead (Bind b) v t
                    assume P: Prop
                      (H_x) 
                         by (iso_gen_head . . . . H0)
ex_2 T T λv2:T.λt2:T.eq T (THead (Bind b) v t) (THead (Flat f1) v2 t2)
                      end of H_x
                      (H1) consider H_x
                      we proceed by induction on H1 to prove P
                         case ex_2_intro : x0:T x1:T H2:eq T (THead (Bind b) v t) (THead (Flat f1) x0 x1) ⇒
                            the thesis becomes P
                               (H3) 
                                  we proceed by induction on H2 to prove 
                                     <λ:T.Prop>
                                       CASE THead (Flat f1) x0 x1 OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                                     case refl_equal : ⇒
                                        the thesis becomes 
                                        <λ:T.Prop>
                                          CASE THead (Bind b) v t OF
                                            TSort ⇒False
                                          | TLRef ⇒False
                                          | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                                           consider I
                                           we proved True

                                              <λ:T.Prop>
                                                CASE THead (Bind b) v t OF
                                                  TSort ⇒False
                                                | TLRef ⇒False
                                                | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False

                                     <λ:T.Prop>
                                       CASE THead (Flat f1) x0 x1 OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead k  ⇒<λ:K.Prop> CASE k OF Bind ⇒True | Flat ⇒False
                               end of H3
                               consider H3
                               we proved 
                                  <λ:T.Prop>
                                    CASE THead (Flat f1) x0 x1 OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead 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
P
                      we proved P
                   we proved 
                      (iso
                          THead (Flat f1) t0 (THeads (Flat f1) t1 (THead (Flat f2) v2 t2))
                          THead (Bind b) v t)
                        →∀P:Prop.P

                      (iso
                          THeads (Flat f1) (TCons t0 t1) (THead (Flat f2) v2 t2)
                          THead (Bind b) v t)
                        →∀P:Prop.P
          we proved 
             (iso
                 THeads (Flat f1) vs (THead (Flat f2) v2 t2)
                 THead (Bind b) v t)
               →∀P:Prop.P
       we proved 
          ∀f1:F
            .∀f2:F
              .∀b:B
                .∀v:T
                  .∀v2:T
                    .∀t:T
                      .∀t2:T
                        .∀vs:TList
                          .(iso
                              THeads (Flat f1) vs (THead (Flat f2) v2 t2)
                              THead (Bind b) v t)
                            →∀P:Prop.P