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 =
        assume P: C→C→Prop
        suppose H: ∀b:B.∀c:C.∀t:T.(P (CHead c (Bind b) t) (CHead c (Bind b) t))
        suppose H1: ∀c:C.∀c1:C.(clear c c1)→(P c c1)→∀f:F.∀t:T.(P (CHead c (Flat f) t) c1)
          (aux) by well-founded reasoning we prove ∀c:C.∀c1:C.(clear c c1)→(P c c1)
           assume c: C
           assume c1: C
           suppose H2: clear c c1
             by cases on H2 we prove P c c1
                case clear_bind b:B c2:C t:T ⇒
                   the thesis becomes P (CHead c2 (Bind b) t) (CHead c2 (Bind b) t)
                   by (H . . .)
P (CHead c2 (Bind b) t) (CHead c2 (Bind b) t)
                case clear_flat c2:C c3:C H3:clear c2 c3 f:F t:T ⇒
                   the thesis becomes P (CHead c2 (Flat f) t) c3
                   by (aux . . H3)
                   we proved P c2 c3
                   by (H1 . . H3 previous . .)
P (CHead c2 (Flat f) t) c3
             we proved P c c1
∀c:C.∀c1:C.(clear c c1)→(P c c1)
          done
          consider aux
          we proved ∀c:C.∀c1:C.(clear c c1)→(P c c1)
       we proved 
          ∀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))