DEFINITION getl_gen_tail()
TYPE =
       ∀k:K
         .∀b:B
           .∀u1:T
             .∀u2:T
               .∀c2:C
                 .∀c1:C
                   .∀i:nat
                     .getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)
                       →(or
                            ex2 C λe:C.eq C c2 (CTail k u1 e) λe:C.getl i c1 (CHead e (Bind b) u2)
                            ex4
                              nat
                              λ:nat.eq nat i (clen c1)
                              λ:nat.eq K k (Bind b)
                              λ:nat.eq T u1 u2
                              λn:nat.eq C c2 (CSort n))
BODY =
Show proof