DEFINITION clear_clear()
TYPE =
       ∀c1:C.∀c2:C.(clear c1 c2)→(clear c2 c2)
BODY =
       assume c1: C
          we proceed by induction on c1 to prove ∀c2:C.(clear c1 c2)→(clear c2 c2)
             case CSort : n:nat ⇒
                the thesis becomes ∀c2:C.∀H:(clear (CSort n) c2).(clear c2 c2)
                    assume c2: C
                    suppose H: clear (CSort n) c2
                      by (clear_gen_sort . . H .)
                      we proved clear c2 c2
∀c2:C.∀H:(clear (CSort n) c2).(clear c2 c2)
             case CHead : c:C k:K t:T ⇒
                the thesis becomes ∀c2:C.∀H0:(clear (CHead c k t) c2).(clear c2 c2)
                (H) by induction hypothesis we know ∀c2:C.(clear c c2)→(clear c2 c2)
                    assume c2: C
                    suppose H0: clear (CHead c k t) c2
                         assume b: B
                         suppose H1: clear (CHead c (Bind b) t) c2
                            (h1) 
                               by (clear_bind . . .)
clear (CHead c (Bind b) t) (CHead c (Bind b) t)
                            end of h1
                            (h2) 
                               by (clear_gen_bind . . . . H1)
eq C c2 (CHead c (Bind b) t)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved clear c2 c2
∀H1:(clear (CHead c (Bind b) t) c2).(clear c2 c2)
                         assume f: F
                         suppose H1: clear (CHead c (Flat f) t) c2
                            by (clear_gen_flat . . . . H1)
                            we proved clear c c2
                            by (H . previous)
                            we proved clear c2 c2
∀H1:(clear (CHead c (Flat f) t) c2).(clear c2 c2)
                      by (previous . H0)
                      we proved clear c2 c2
∀c2:C.∀H0:(clear (CHead c k t) c2).(clear c2 c2)
          we proved ∀c2:C.(clear c1 c2)→(clear c2 c2)
       we proved ∀c1:C.∀c2:C.(clear c1 c2)→(clear c2 c2)