DEFINITION lifts1_flat()
TYPE =
       ∀f:F
         .∀hds:PList
           .∀t:T
             .∀ts:TList
               .eq
                 T
                 lift1 hds (THeads (Flat f) ts t)
                 THeads (Flat f) (lifts1 hds ts) (lift1 hds t)
BODY =
        assume f: F
        assume hds: PList
        assume t: T
        assume ts: TList
          we proceed by induction on ts to prove 
             eq
               T
               lift1 hds (THeads (Flat f) ts t)
               THeads (Flat f) (lifts1 hds ts) (lift1 hds t)
             case TNil : ⇒
                the thesis becomes 
                eq
                  T
                  lift1 hds (THeads (Flat f) TNil t)
                  THeads (Flat f) (lifts1 hds TNil) (lift1 hds t)
                   by (refl_equal . .)
                   we proved eq T (lift1 hds t) (lift1 hds t)

                      eq
                        T
                        lift1 hds (THeads (Flat f) TNil t)
                        THeads (Flat f) (lifts1 hds TNil) (lift1 hds t)
             case TCons : t0:T t1:TList ⇒
                the thesis becomes 
                eq
                  T
                  lift1 hds (THeads (Flat f) (TCons t0 t1) t)
                  THeads (Flat f) (lifts1 hds (TCons t0 t1)) (lift1 hds t)
                (H) by induction hypothesis we know 
                   eq
                     T
                     lift1 hds (THeads (Flat f) t1 t)
                     THeads (Flat f) (lifts1 hds t1) (lift1 hds t)
                   (h1) 
                      by (refl_equal . .)
                      we proved 
                         eq
                           T
                           THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t))
                           THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t))
                      by (eq_ind_r . . . previous . H)

                         eq
                           T
                           THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f) t1 t))
                           THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t))
                   end of h1
                   (h2) 
                      by (lift1_flat . . . .)

                         eq
                           T
                           lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))
                           THead (Flat f) (lift1 hds t0) (lift1 hds (THeads (Flat f) t1 t))
                   end of h2
                   by (eq_ind_r . . . h1 . h2)
                   we proved 
                      eq
                        T
                        lift1 hds (THead (Flat f) t0 (THeads (Flat f) t1 t))
                        THead (Flat f) (lift1 hds t0) (THeads (Flat f) (lifts1 hds t1) (lift1 hds t))

                      eq
                        T
                        lift1 hds (THeads (Flat f) (TCons t0 t1) t)
                        THeads (Flat f) (lifts1 hds (TCons t0 t1)) (lift1 hds t)
          we proved 
             eq
               T
               lift1 hds (THeads (Flat f) ts t)
               THeads (Flat f) (lifts1 hds ts) (lift1 hds t)
       we proved 
          ∀f:F
            .∀hds:PList
              .∀t:T
                .∀ts:TList
                  .eq
                    T
                    lift1 hds (THeads (Flat f) ts t)
                    THeads (Flat f) (lifts1 hds ts) (lift1 hds t)