DEFINITION cimp_flat_sx()
TYPE =
       ∀f:F.∀c:C.∀v:T.(cimp (CHead c (Flat f) v) c)
BODY =
        assume f: F
        assume c: C
        assume v: T
          we must prove cimp (CHead c (Flat f) v) c
          or equivalently 
                ∀b:B
                  .∀d1:C
                    .∀w:T
                      .∀h:nat
                        .getl h (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                          →ex C λd2:C.getl h c (CHead d2 (Bind b) w)
           assume b: B
           assume d1: C
           assume w: T
           assume h: nat
           suppose H: getl h (CHead c (Flat f) v) (CHead d1 (Bind b) w)
             suppose H0: getl O (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                (h1) 
                   by (drop_refl .)
drop O O c c
                end of h1
                (h2) 
                   by (getl_gen_O . . H0)
                   we proved clear (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                   by (clear_gen_flat . . . . previous)
clear c (CHead d1 (Bind b) w)
                end of h2
                by (getl_intro . . . . h1 h2)
                we proved getl O c (CHead d1 (Bind b) w)
                by (ex_intro . . . previous)
                we proved ex C λd2:C.getl O c (CHead d2 (Bind b) w)

                getl O (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                  →ex C λd2:C.getl O c (CHead d2 (Bind b) w)
              assume h0: nat
                 suppose : 
                    getl h0 (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                      →ex C λd2:C.getl h0 c (CHead d2 (Bind b) w)
                suppose H0: getl (S h0) (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                   by (getl_gen_S . . . . . H0)
                   we proved getl (r (Flat f) h0) c (CHead d1 (Bind b) w)
                   that is equivalent to getl (S h0) c (CHead d1 (Bind b) w)
                   by (ex_intro . . . previous)
                   we proved ex C λd2:C.getl (S h0) c (CHead d2 (Bind b) w)

                   ∀H0:getl (S h0) (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                     .ex C λd2:C.getl (S h0) c (CHead d2 (Bind b) w)
             by (previous . H)
             we proved ex C λd2:C.getl h c (CHead d2 (Bind b) w)
          we proved 
             ∀b:B
               .∀d1:C
                 .∀w:T
                   .∀h:nat
                     .getl h (CHead c (Flat f) v) (CHead d1 (Bind b) w)
                       →ex C λd2:C.getl h c (CHead d2 (Bind b) w)
          that is equivalent to cimp (CHead c (Flat f) v) c
       we proved ∀f:F.∀c:C.∀v:T.(cimp (CHead c (Flat f) v) c)