DEFINITION getl_flat()
TYPE =
       ∀c:C.∀e:C.∀h:nat.(getl h c e)→∀f:F.∀u:T.(getl h (CHead c (Flat f) u) e)
BODY =
        assume c: C
        assume e: C
        assume h: nat
        suppose H: getl h c e
        assume f: F
        assume u: T
          (H0) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop h O c e λe:C.clear e e
          end of H0
          we proceed by induction on H0 to prove getl h (CHead c (Flat f) u) e
             case ex_intro2 : x:C H1:drop h O c x H2:clear x e ⇒
                the thesis becomes getl h (CHead c (Flat f) u) e
                   suppose H3: drop O O c x
                      (H4) 
                         by (drop_gen_refl . . H3)
                         we proved eq C c x
                         by (eq_ind_r . . . H2 . previous)
clear c e
                      end of H4
                      (h1) 
                         by (drop_refl .)
drop O O (CHead c (Flat f) u) (CHead c (Flat f) u)
                      end of h1
                      (h2) 
                         by (clear_flat . . H4 . .)
clear (CHead c (Flat f) u) e
                      end of h2
                      by (getl_intro . . . . h1 h2)
                      we proved getl O (CHead c (Flat f) u) e
(drop O O c x)→(getl O (CHead c (Flat f) u) e)
                    assume h0: nat
                       suppose : (drop h0 O c x)→(getl h0 (CHead c (Flat f) u) e)
                      suppose H3: drop (S h0) O c x
                         consider H3
                         we proved drop (S h0) O c x
                         that is equivalent to drop (r (Flat f) h0) O c x
                         by (drop_drop . . . . previous .)
                         we proved drop (S h0) O (CHead c (Flat f) u) x
                         by (getl_intro . . . . previous H2)
                         we proved getl (S h0) (CHead c (Flat f) u) e
∀H3:(drop (S h0) O c x).(getl (S h0) (CHead c (Flat f) u) e)
                   by (previous . H1)
getl h (CHead c (Flat f) u) e
          we proved getl h (CHead c (Flat f) u) e
       we proved ∀c:C.∀e:C.∀h:nat.(getl h c e)→∀f:F.∀u:T.(getl h (CHead c (Flat f) u) e)