DEFINITION csubst0_clear_O_back()
TYPE =
       ∀c1:C.∀c2:C.∀v:T.(csubst0 O v c1 c2)→∀c:C.(clear c2 c)→(clear c1 c)
BODY =
Show proof