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