DEFINITION clear_gen_all()
TYPE =
       ∀c1:C.∀c2:C.(clear c1 c2)→(ex_3 B C T λb:B.λe:C.λu:T.eq C c2 (CHead e (Bind b) u))
BODY =
        assume c1: C
        assume c2: C
        suppose H: clear c1 c2
          we proceed by induction on H to prove ex_3 B C T λb:B.λe:C.λu:T.eq C c2 (CHead e (Bind b) u)
             case clear_bind : b:B e:C u:T ⇒
                the thesis becomes ex_3 B C T λb0:B.λe0:C.λu0:T.eq C (CHead e (Bind b) u) (CHead e0 (Bind b0) u0)
                   by (refl_equal . .)
                   we proved eq C (CHead e (Bind b) u) (CHead e (Bind b) u)
                   by (ex_3_intro . . . . . . . previous)
ex_3 B C T λb0:B.λe0:C.λu0:T.eq C (CHead e (Bind b) u) (CHead e0 (Bind b0) u0)
             case clear_flat : e:C c:C H0:clear e c :F :T ⇒
                the thesis becomes ex_3 B C T λb:B.λe0:C.λu0:T.eq C c (CHead e0 (Bind b) u0)
                (H1) by induction hypothesis we know ex_3 B C T λb:B.λe0:C.λu:T.eq C c (CHead e0 (Bind b) u)
                   (H2) consider H1
                   we proceed by induction on H2 to prove ex_3 B C T λb:B.λe0:C.λu0:T.eq C c (CHead e0 (Bind b) u0)
                      case ex_3_intro : x0:B x1:C x2:T H3:eq C c (CHead x1 (Bind x0) x2) ⇒
                         the thesis becomes ex_3 B C T λb:B.λe0:C.λu0:T.eq C c (CHead e0 (Bind b) u0)
                            by (refl_equal . .)
                            we proved eq C (CHead x1 (Bind x0) x2) (CHead x1 (Bind x0) x2)
                            by (ex_3_intro . . . . . . . previous)
                            we proved ex_3 B C T λb:B.λe0:C.λu0:T.eq C (CHead x1 (Bind x0) x2) (CHead e0 (Bind b) u0)
                            by (eq_ind_r . . . previous . H3)
ex_3 B C T λb:B.λe0:C.λu0:T.eq C c (CHead e0 (Bind b) u0)
ex_3 B C T λb:B.λe0:C.λu0:T.eq C c (CHead e0 (Bind b) u0)
          we proved ex_3 B C T λb:B.λe:C.λu:T.eq C c2 (CHead e (Bind b) u)
       we proved ∀c1:C.∀c2:C.(clear c1 c2)→(ex_3 B C T λb:B.λe:C.λu:T.eq C c2 (CHead e (Bind b) u))