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