DEFINITION cimp_flat_dx()
TYPE =
       ∀f:F.∀c:C.∀v:T.(cimp c (CHead c (Flat f) v))
BODY =
        assume f: F
        assume c: C
        assume v: T
          we must prove cimp c (CHead c (Flat f) v)
          or equivalently 
                ∀b:B
                  .∀d1:C
                    .∀w:T
                      .∀h:nat
                        .getl h c (CHead d1 (Bind b) w)
                          →ex C λd2:C.getl h (CHead c (Flat f) v) (CHead d2 (Bind b) w)
           assume b: B
           assume d1: C
           assume w: T
           assume h: nat
           suppose H: getl h c (CHead d1 (Bind b) w)
             by (getl_flat . . . H . .)
             we proved getl h (CHead c (Flat f) v) (CHead d1 (Bind b) w)
             by (ex_intro . . . previous)
             we proved ex C λd2:C.getl h (CHead c (Flat f) v) (CHead d2 (Bind b) w)
          we proved 
             ∀b:B
               .∀d1:C
                 .∀w:T
                   .∀h:nat
                     .getl h c (CHead d1 (Bind b) w)
                       →ex C λd2:C.getl h (CHead c (Flat f) v) (CHead d2 (Bind b) w)
          that is equivalent to cimp c (CHead c (Flat f) v)
       we proved ∀f:F.∀c:C.∀v:T.(cimp c (CHead c (Flat f) v))