DEFINITION lift1_flat()
TYPE =
       ∀f:F
         .∀hds:PList
           .∀u:T
             .∀t:T
               .eq
                 T
                 lift1 hds (THead (Flat f) u t)
                 THead (Flat f) (lift1 hds u) (lift1 hds t)
BODY =
        assume f: F
        assume hds: PList
          we proceed by induction on hds to prove 
             ∀u:T
               .∀t:T
                 .eq
                   T
                   lift1 hds (THead (Flat f) u t)
                   THead (Flat f) (lift1 hds u) (lift1 hds t)
             case PNil : ⇒
                the thesis becomes 
                ∀u:T
                  .∀t:T
                    .eq
                      T
                      lift1 PNil (THead (Flat f) u t)
                      THead (Flat f) (lift1 PNil u) (lift1 PNil t)
                    assume u: T
                    assume t: T
                      by (refl_equal . .)
                      we proved eq T (THead (Flat f) u t) (THead (Flat f) u t)
                      that is equivalent to 
                         eq
                           T
                           lift1 PNil (THead (Flat f) u t)
                           THead (Flat f) (lift1 PNil u) (lift1 PNil t)

                      ∀u:T
                        .∀t:T
                          .eq
                            T
                            lift1 PNil (THead (Flat f) u t)
                            THead (Flat f) (lift1 PNil u) (lift1 PNil t)
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes 
                ∀u:T
                  .∀t:T
                    .eq
                      T
                      lift n n0 (lift1 p (THead (Flat f) u t))
                      THead (Flat f) (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t))
                (H) by induction hypothesis we know 
                   ∀u:T
                     .∀t:T
                       .eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))
                    assume u: T
                    assume t: T
                      (h1) 
                         (h1) 
                            by (refl_equal . .)

                               eq
                                 T
                                 THead (Flat f) (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t))
                                 THead (Flat f) (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t))
                         end of h1
                         (h2) 
                            by (lift_flat . . . . .)

                               eq
                                 T
                                 lift n n0 (THead (Flat f) (lift1 p u) (lift1 p t))
                                 THead (Flat f) (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t))
                         end of h2
                         by (eq_ind_r . . . h1 . h2)

                            eq
                              T
                              lift n n0 (THead (Flat f) (lift1 p u) (lift1 p t))
                              THead (Flat f) (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t))
                      end of h1
                      (h2) 
                         by (H . .)
eq T (lift1 p (THead (Flat f) u t)) (THead (Flat f) (lift1 p u) (lift1 p t))
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         eq
                           T
                           lift n n0 (lift1 p (THead (Flat f) u t))
                           THead (Flat f) (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t))
                      that is equivalent to 
                         eq
                           T
                           lift1 (PCons n n0 p) (THead (Flat f) u t)
                           THead (Flat f) (lift1 (PCons n n0 p) u) (lift1 (PCons n n0 p) t)

                      ∀u:T
                        .∀t:T
                          .eq
                            T
                            lift n n0 (lift1 p (THead (Flat f) u t))
                            THead (Flat f) (lift n n0 (lift1 p u)) (lift n n0 (lift1 p t))
          we proved 
             ∀u:T
               .∀t:T
                 .eq
                   T
                   lift1 hds (THead (Flat f) u t)
                   THead (Flat f) (lift1 hds u) (lift1 hds t)
       we proved 
          ∀f:F
            .∀hds:PList
              .∀u:T
                .∀t:T
                  .eq
                    T
                    lift1 hds (THead (Flat f) u t)
                    THead (Flat f) (lift1 hds u) (lift1 hds t)