DEFINITION lift_gen_flat()
TYPE =
       ∀f:F
         .∀u:T
           .∀t:T
             .∀x:T
               .∀h:nat
                 .∀d:nat
                   .eq T (THead (Flat f) u t) (lift h d x)
                     →(ex3_2
                          T
                          T
                          λy:T.λz:T.eq T x (THead (Flat f) y z)
                          λy:T.λ:T.eq T u (lift h d y)
                          λ:T.λz:T.eq T t (lift h d z))
BODY =
Show proof