DEFINITION clear_cle()
TYPE =
       ∀c1:C.∀c2:C.(clear c1 c2)→(cle c2 c1)
BODY =
       assume c1: C
          we proceed by induction on c1 to prove ∀c2:C.(clear c1 c2)→(le (cweight c2) (cweight c1))
             case CSort : n:nat ⇒
                the thesis becomes ∀c2:C.∀H:(clear (CSort n) c2).(le (cweight c2) O)
                    assume c2: C
                    suppose H: clear (CSort n) c2
                      by (clear_gen_sort . . H .)
                      we proved le (cweight c2) O
                      that is equivalent to le (cweight c2) (cweight (CSort n))
∀c2:C.∀H:(clear (CSort n) c2).(le (cweight c2) O)
             case CHead : c:C k:K t:T ⇒
                the thesis becomes 
                ∀c2:C
                  .∀H0:clear (CHead c k t) c2
                    .le (cweight c2) (plus (cweight c) (tweight t))
                (H) by induction hypothesis we know ∀c2:C.(clear c c2)→(le (cweight c2) (cweight c))
                    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 (le_n .)
                               we proved 
                                  le
                                    plus (cweight c) (tweight t)
                                    plus (cweight c) (tweight t)

                                  le
                                    cweight (CHead c (Bind b) t)
                                    plus (cweight c) (tweight 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 le (cweight c2) (plus (cweight c) (tweight t))

                            ∀H1:clear (CHead c (Bind b) t) c2
                              .le (cweight c2) (plus (cweight c) (tweight t))
                         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 le (cweight c2) (cweight c)
                            by (le_plus_trans . . . previous)
                            we proved le (cweight c2) (plus (cweight c) (tweight t))

                            ∀H1:clear (CHead c (Flat f) t) c2
                              .le (cweight c2) (plus (cweight c) (tweight t))
                      by (previous . H0)
                      we proved le (cweight c2) (plus (cweight c) (tweight t))
                      that is equivalent to le (cweight c2) (cweight (CHead c k t))

                      ∀c2:C
                        .∀H0:clear (CHead c k t) c2
                          .le (cweight c2) (plus (cweight c) (tweight t))
          we proved ∀c2:C.(clear c1 c2)→(le (cweight c2) (cweight c1))
          that is equivalent to ∀c2:C.(clear c1 c2)→(cle c2 c1)
       we proved ∀c1:C.∀c2:C.(clear c1 c2)→(cle c2 c1)