DEFINITION iso_flats_lref_bind_false()
TYPE =
       ∀f:F
         .∀b:B
           .∀i:nat
             .∀v:T
               .∀t:T
                 .∀vs:TList
                   .iso (THeads (Flat f) vs (TLRef i)) (THead (Bind b) v t)
                     →∀P:Prop.P
BODY =
        assume f: F
        assume b: B
        assume i: nat
        assume v: T
        assume t: T
        assume vs: TList
          we proceed by induction on vs to prove 
             iso (THeads (Flat f) vs (TLRef i)) (THead (Bind b) v t)
               →∀P:Prop.P
             case TNil : ⇒
                the thesis becomes 
                iso (THeads (Flat f) TNil (TLRef i)) (THead (Bind b) v t)
                  →∀P:Prop.P
                   we must prove 
                         iso (THeads (Flat f) TNil (TLRef i)) (THead (Bind b) v t)
                           →∀P:Prop.P
                   or equivalently (iso (TLRef i) (THead (Bind b) v t))→∀P:Prop.P
                    suppose H: iso (TLRef i) (THead (Bind b) v t)
                    assume P: Prop
                      (H_x) 
                         by (iso_gen_lref . . H)
ex nat λn2:nat.eq T (THead (Bind b) v t) (TLRef n2)
                      end of H_x
                      (H0) consider H_x
                      we proceed by induction on H0 to prove P
                         case ex_intro : x:nat H1:eq T (THead (Bind b) v t) (TLRef x) ⇒
                            the thesis becomes P
                               (H2) 
                                  we proceed by induction on H1 to prove 
                                     <λ:T.Prop>
                                       CASE TLRef x OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead   ⇒True
                                     case refl_equal : ⇒
                                        the thesis becomes 
                                        <λ:T.Prop>
                                          CASE THead (Bind b) v t OF
                                            TSort ⇒False
                                          | TLRef ⇒False
                                          | THead   ⇒True
                                           consider I
                                           we proved True

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

                                     <λ:T.Prop>
                                       CASE TLRef x OF
                                         TSort ⇒False
                                       | TLRef ⇒False
                                       | THead   ⇒True
                               end of H2
                               consider H2
                               we proved 
                                  <λ:T.Prop>
                                    CASE TLRef x OF
                                      TSort ⇒False
                                    | TLRef ⇒False
                                    | THead   ⇒True
                               that is equivalent to False
                               we proceed by induction on the previous result to prove P
P
                      we proved P
                   we proved (iso (TLRef i) (THead (Bind b) v t))→∀P:Prop.P

                      iso (THeads (Flat f) TNil (TLRef i)) (THead (Bind b) v t)
                        →∀P:Prop.P
             case TCons : t0:T t1:TList ⇒
                the thesis becomes 
                (iso
                    THeads (Flat f) (TCons t0 t1) (TLRef i)
                    THead (Bind b) v t)
                  →∀P:Prop.P
                () by induction hypothesis we know 
                   iso (THeads (Flat f) t1 (TLRef i)) (THead (Bind b) v t)
                     →∀P:Prop.P
                   we must prove 
                         (iso
                             THeads (Flat f) (TCons t0 t1) (TLRef i)
                             THead (Bind b) v t)
                           →∀P:Prop.P
                   or equivalently 
                         (iso
                             THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))
                             THead (Bind b) v t)
                           →∀P:Prop.P
                    suppose H0: 
                       iso
                         THead (Flat f) t0 (THeads (Flat f) t1 (TLRef i))
                         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 f) 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 f) x0 x1) ⇒
                            the thesis becomes P
                               (H3) 
                                  we proceed by induction on H2 to prove 
                                     <λ:T.Prop>
                                       CASE THead (Flat f) 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 f) 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 f) 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 f) t0 (THeads (Flat f) t1 (TLRef i))
                          THead (Bind b) v t)
                        →∀P:Prop.P

                      (iso
                          THeads (Flat f) (TCons t0 t1) (TLRef i)
                          THead (Bind b) v t)
                        →∀P:Prop.P
          we proved 
             iso (THeads (Flat f) vs (TLRef i)) (THead (Bind b) v t)
               →∀P:Prop.P
       we proved 
          ∀f:F
            .∀b:B
              .∀i:nat
                .∀v:T
                  .∀t:T
                    .∀vs:TList
                      .iso (THeads (Flat f) vs (TLRef i)) (THead (Bind b) v t)
                        →∀P:Prop.P