DEFINITION clear_ind()
TYPE =
       ∀P:C→C→Prop
         .∀b:B.∀c:C.∀t:T.(P (CHead c (Bind b) t) (CHead c (Bind b) t))
           →(∀c:C.∀c1:C.(clear c c1)→(P c c1)→∀f:F.∀t:T.(P (CHead c (Flat f) t) c1)
                →∀c:C.∀c1:C.(clear c c1)→(P c c1))
BODY =
Show proof