DEFINITION csubt_drop_flat()
TYPE =
       ∀g:G
         .∀f:F
           .∀n:nat
             .∀c1:C
               .∀c2:C
                 .csubt g c1 c2
                   →∀d1:C
                        .∀u:T
                          .drop n O c1 (CHead d1 (Flat f) u)
                            →ex2 C λd2:C.csubt g d1 d2 λd2:C.drop n O c2 (CHead d2 (Flat f) u)
BODY =
Show proof