DEFINITION lift_flat()
TYPE =
       ∀f:F
         .∀u:T
           .∀t:T
             .∀h:nat
               .∀d:nat
                 .eq
                   T
                   lift h d (THead (Flat f) u t)
                   THead (Flat f) (lift h d u) (lift h d t)
BODY =
        assume f: F
        assume u: T
        assume t: T
        assume h: nat
        assume d: nat
          by (refl_equal . .)
          we proved 
             eq
               T
               THead (Flat f) (lift h d u) (lift h d t)
               THead (Flat f) (lift h d u) (lift h d t)
          that is equivalent to 
             eq
               T
               lift h d (THead (Flat f) u t)
               THead (Flat f) (lift h d u) (lift h d t)
       we proved 
          ∀f:F
            .∀u:T
              .∀t:T
                .∀h:nat
                  .∀d:nat
                    .eq
                      T
                      lift h d (THead (Flat f) u t)
                      THead (Flat f) (lift h d u) (lift h d t)