DEFINITION csubst0_drop_lt()
TYPE =
       ∀n:nat
         .∀i:nat
           .lt n i
             →∀c1:C
                  .∀c2:C
                    .∀v:T
                      .csubst0 i v c1 c2
                        →∀e:C
                             .drop n O c1 e
                               →(or4
                                    drop n O c2 e
                                    ex3_4
                                      K
                                      C
                                      T
                                      T
                                      λk:K.λe0:C.λu:T.λ:T.eq C e (CHead e0 k u)
                                      λk:K.λe0:C.λ:T.λw:T.drop n O c2 (CHead e0 k w)
                                      λk:K.λ:C.λu:T.λw:T.subst0 (minus i (s k n)) v u w
                                    ex3_4
                                      K
                                      C
                                      C
                                      T
                                      λk:K.λe1:C.λ:C.λu:T.eq C e (CHead e1 k u)
                                      λk:K.λ:C.λe2:C.λu:T.drop n O c2 (CHead e2 k u)
                                      λk:K.λe1:C.λe2:C.λ:T.csubst0 (minus i (s k n)) v e1 e2
                                    ex4_5
                                      K
                                      C
                                      C
                                      T
                                      T
                                      λk:K.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 k u)
                                      λk:K.λ:C.λe2:C.λ:T.λw:T.drop n O c2 (CHead e2 k w)
                                      λk:K.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (s k n)) v u w
                                      λk:K.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (s k n)) v e1 e2)
BODY =
Show proof