DEFINITION csubst0_getl_lt()
TYPE =
       ∀i:nat
         .∀n:nat
           .lt n i
             →∀c1:C
                  .∀c2:C
                    .∀v:T
                      .csubst0 i v c1 c2
                        →∀e:C
                             .getl n c1 e
                               →(or4
                                    getl n c2 e
                                    ex3_4
                                      B
                                      C
                                      T
                                      T
                                      λb:B.λe0:C.λu:T.λ:T.eq C e (CHead e0 (Bind b) u)
                                      λb:B.λe0:C.λ:T.λw:T.getl n c2 (CHead e0 (Bind b) w)
                                      λ:B.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
                                    ex3_4
                                      B
                                      C
                                      C
                                      T
                                      λb:B.λe1:C.λ:C.λu:T.eq C e (CHead e1 (Bind b) u)
                                      λb:B.λ:C.λe2:C.λu:T.getl n c2 (CHead e2 (Bind b) u)
                                      λ:B.λe1:C.λe2:C.λ:T.csubst0 (minus i (S n)) v e1 e2
                                    ex4_5
                                      B
                                      C
                                      C
                                      T
                                      T
                                      λb:B.λe1:C.λ:C.λu:T.λ:T.eq C e (CHead e1 (Bind b) u)
                                      λb:B.λ:C.λe2:C.λ:T.λw:T.getl n c2 (CHead e2 (Bind b) w)
                                      λ:B.λ:C.λ:C.λu:T.λw:T.subst0 (minus i (S n)) v u w
                                      λ:B.λe1:C.λe2:C.λ:T.λ:T.csubst0 (minus i (S n)) v e1 e2)
BODY =
Show proof