DEFINITION getl_clear_bind()
TYPE =
       ∀b:B
         .∀c:C
           .∀e1:C
             .∀v:T
               .clear c (CHead e1 (Bind b) v)
                 →∀e2:C.∀n:nat.(getl n e1 e2)→(getl (S n) c e2)
BODY =
Show proof