DEFINITION csubst0_drop_eq_back()
TYPE =
       ∀n:nat
         .∀c1:C
           .∀c2:C
             .∀v:T
               .csubst0 n v c1 c2
                 →∀e:C
                      .drop n O c2 e
                        →(or4
                             drop n O c1 e
                             ex3_4
                               F
                               C
                               T
                               T
                               λf:F.λe0:C.λ:T.λu2:T.eq C e (CHead e0 (Flat f) u2)
                               λf:F.λe0:C.λu1:T.λ:T.drop n O c1 (CHead e0 (Flat f) u1)
                               λ:F.λ:C.λu1:T.λu2:T.subst0 O v u1 u2
                             ex3_4
                               F
                               C
                               C
                               T
                               λf:F.λ:C.λe2:C.λu:T.eq C e (CHead e2 (Flat f) u)
                               λf:F.λe1:C.λ:C.λu:T.drop n O c1 (CHead e1 (Flat f) u)
                               λ:F.λe1:C.λe2:C.λ:T.csubst0 O v e1 e2
                             ex4_5
                               F
                               C
                               C
                               T
                               T
                               λf:F.λ:C.λe2:C.λ:T.λu2:T.eq C e (CHead e2 (Flat f) u2)
                               λf:F.λe1:C.λ:C.λu1:T.λ:T.drop n O c1 (CHead e1 (Flat f) u1)
                               λ:F.λ:C.λ:C.λu1:T.λu2:T.subst0 O v u1 u2
                               λ:F.λe1:C.λe2:C.λ:T.λ:T.csubst0 O v e1 e2)
BODY =
Show proof