DEFINITION getl_flt()
TYPE =
       ∀b:B
         .∀c:C
           .∀e:C
             .∀u:T
               .∀i:nat.(getl i c (CHead e (Bind b) u))→(flt e u c (TLRef i))
BODY =
Show proof