DEFINITION csubst0_gen_S_bind_2()
TYPE =
       ∀b:B
         .∀x:C
           .∀c2:C
             .∀v:T
               .∀v2:T
                 .∀i:nat
                   .csubst0 (S i) v x (CHead c2 (Bind b) v2)
                     →(or3
                          ex2 T λv1:T.subst0 i v v1 v2 λv1:T.eq C x (CHead c2 (Bind b) v1)
                          ex2 C λc1:C.csubst0 i v c1 c2 λc1:C.eq C x (CHead c1 (Bind b) v2)
                          ex3_2 C T λ:C.λv1:T.subst0 i v v1 v2 λc1:C.λ:T.csubst0 i v c1 c2 λc1:C.λv1:T.eq C x (CHead c1 (Bind b) v1))
BODY =
Show proof