DEFINITION getl_gen_bind()
TYPE =
       ∀b:B
         .∀e:C
           .∀d:C
             .∀v:T
               .∀i:nat
                 .getl i (CHead e (Bind b) v) d
                   →(or
                        land (eq nat i O) (eq C d (CHead e (Bind b) v))
                        ex2 nat λj:nat.eq nat i (S j) λj:nat.getl j e d)
BODY =
Show proof