DEFINITION wf3_gen_bind1()
TYPE =
       ∀g:G
         .∀c1:C
           .∀x:C
             .∀v:T
               .∀b:B
                 .wf3 g (CHead c1 (Bind b) v) x
                   →(or
                        ex3_2 C T λc2:C.λ:T.eq C x (CHead c2 (Bind b) v) λc2:C.λ:T.wf3 g c1 c2 λ:C.λw:T.ty3 g c1 v w
                        ex3
                          C
                          λc2:C.eq C x (CHead c2 (Bind Void) (TSort O))
                          λc2:C.wf3 g c1 c2
                          λ:C.∀w:T.(ty3 g c1 v w)→False)
BODY =
Show proof