DEFINITION csubst0_clear_trans()
TYPE =
       ∀c1:C
         .∀c2:C
           .∀v:T
             .∀i:nat
               .csubst0 i v c1 c2
                 →∀e2:C.(clear c2 e2)→(or (clear c1 e2) (ex2 C λe1:C.csubst0 i v e1 e2 λe1:C.clear c1 e1))
BODY =
Show proof