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