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 =
Show proof