DEFINITION drop_skip_flat()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀c:C
             .∀e:C
               .drop h (S d) c e
                 →∀f:F
                      .∀u:T
                        .drop
                          h
                          S d
                          CHead c (Flat f) (lift h (S d) u)
                          CHead e (Flat f) u
BODY =
Show proof