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 =
Show proof