DEFINITION getl_dec()
TYPE =
       ∀c:C
         .∀i:nat
           .or
             ex_3 C B T λe:C.λb:B.λv:T.getl i c (CHead e (Bind b) v)
             ∀d:C.(getl i c d)→∀P:Prop.P
BODY =
Show proof