DEFINITION csubst0_clear_S()
TYPE =
       ∀c1:C
         .∀c2:C
           .∀v:T
             .∀i:nat
               .csubst0 (S i) v c1 c2
                 →∀c:C
                      .clear c1 c
                        →(or4
                             clear c2 c
                             ex3_4
                               B
                               C
                               T
                               T
                               λb:B.λe:C.λu1:T.λ:T.eq C c (CHead e (Bind b) u1)
                               λb:B.λe:C.λ:T.λu2:T.clear c2 (CHead e (Bind b) u2)
                               λ:B.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
                             ex3_4
                               B
                               C
                               C
                               T
                               λb:B.λe1:C.λ:C.λu:T.eq C c (CHead e1 (Bind b) u)
                               λb:B.λ:C.λe2:C.λu:T.clear c2 (CHead e2 (Bind b) u)
                               λ:B.λe1:C.λe2:C.λ:T.csubst0 i v e1 e2
                             ex4_5
                               B
                               C
                               C
                               T
                               T
                               λb:B.λe1:C.λ:C.λu1:T.λ:T.eq C c (CHead e1 (Bind b) u1)
                               λb:B.λ:C.λe2:C.λ:T.λu2:T.clear c2 (CHead e2 (Bind b) u2)
                               λ:B.λ:C.λ:C.λu1:T.λu2:T.subst0 i v u1 u2
                               λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 i v e1 e2)
BODY =
Show proof