DEFINITION getl_csubst1()
TYPE =
       ∀d:nat
         .∀c:C
           .∀e:C
             .∀u:T
               .getl d c (CHead e (Bind Abbr) u)
                 →ex2_2 C C λa0:C.λ:C.csubst1 d u c a0 λa0:C.λa:C.drop (S O) d a0 a
BODY =
Show proof