DEFINITION getl_gen_flat()
TYPE =
       ∀f:F.∀e:C.∀d:C.∀v:T.∀i:nat.(getl i (CHead e (Flat f) v) d)→(getl i e d)
BODY =
        assume f: F
        assume e: C
        assume d: C
        assume v: T
        assume i: nat
          we proceed by induction on i to prove (getl i (CHead e (Flat f) v) d)→(getl i e d)
             case O : ⇒
                the thesis becomes (getl O (CHead e (Flat f) v) d)→(getl O e d)
                   suppose H: getl O (CHead e (Flat f) v) d
                      (h1) 
                         by (drop_refl .)
drop O O e e
                      end of h1
                      (h2) 
                         by (getl_gen_O . . H)
                         we proved clear (CHead e (Flat f) v) d
                         by (clear_gen_flat . . . . previous)
clear e d
                      end of h2
                      by (getl_intro . . . . h1 h2)
                      we proved getl O e d
(getl O (CHead e (Flat f) v) d)→(getl O e d)
             case S : n:nat ⇒
                the thesis becomes ∀H0:(getl (S n) (CHead e (Flat f) v) d).(getl (r (Flat f) n) e d)
                () by induction hypothesis we know (getl n (CHead e (Flat f) v) d)→(getl n e d)
                   suppose H0: getl (S n) (CHead e (Flat f) v) d
                      by (getl_gen_S . . . . . H0)
                      we proved getl (r (Flat f) n) e d
                      that is equivalent to getl (S n) e d
∀H0:(getl (S n) (CHead e (Flat f) v) d).(getl (r (Flat f) n) e d)
          we proved (getl i (CHead e (Flat f) v) d)→(getl i e d)
       we proved ∀f:F.∀e:C.∀d:C.∀v:T.∀i:nat.(getl i (CHead e (Flat f) v) d)→(getl i e d)