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

                            ∀H2:clear (CHead c0 (Bind b) t) c1
                              .∀H3:(clear (CHead c0 (Bind b) t) c2).(eq C c1 c2)
                         assume f: F
                          suppose H2: clear (CHead c0 (Flat f) t) c1
                          suppose H3: clear (CHead c0 (Flat f) t) c2
                            (h1) 
                               by (clear_gen_flat . . . . H2)
clear c0 c1
                            end of h1
                            (h2) 
                               by (clear_gen_flat . . . . H3)
clear c0 c2
                            end of h2
                            by (H . h1 . h2)
                            we proved eq C c1 c2

                            ∀H2:clear (CHead c0 (Flat f) t) c1
                              .∀H3:(clear (CHead c0 (Flat f) t) c2).(eq C c1 c2)
                      by (previous . H0 H1)
                      we proved eq C c1 c2
∀c1:C.∀H0:(clear (CHead c0 k t) c1).∀c2:C.∀H1:(clear (CHead c0 k t) c2).(eq C c1 c2)
          we proved ∀c1:C.(clear c c1)→∀c2:C.(clear c c2)→(eq C c1 c2)
       we proved ∀c:C.∀c1:C.(clear c c1)→∀c2:C.(clear c c2)→(eq C c1 c2)