DEFINITION csubc_gen_head_l()
TYPE =
       ∀g:G
         .∀c1:C
           .∀x:C
             .∀v:T
               .∀k:K
                 .csubc g (CHead c1 k v) x
                   →(or3
                        ex2 C λc2:C.eq C x (CHead c2 k v) λc2:C.csubc g c1 c2
                        ex5_3
                          C
                          T
                          A
                          λ:C.λ:T.λ:A.eq K k (Bind Abst)
                          λc2:C.λw:T.λ:A.eq C x (CHead c2 (Bind Abbr) w)
                          λc2:C.λ:T.λ:A.csubc g c1 c2
                          λ:C.λ:T.λa:A.sc3 g (asucc g a) c1 v
                          λc2:C.λw:T.λa:A.sc3 g a c2 w
                        ex4_3
                          B
                          C
                          T
                          λb:B.λc2:C.λv2:T.eq C x (CHead c2 (Bind b) v2)
                          λ:B.λ:C.λ:T.eq K k (Bind Void)
                          λb:B.λ:C.λ:T.not (eq B b Void)
                          λ:B.λc2:C.λ:T.csubc g c1 c2)
BODY =
Show proof