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