DEFINITION wf3_clear_conf()
TYPE =
       ∀c1:C.∀c:C.(clear c1 c)→∀g:G.∀c2:C.(wf3 g c1 c2)→(wf3 g c c2)
BODY =
        assume c1: C
        assume c: C
        suppose H: clear c1 c
          we proceed by induction on H to prove ∀g:G.∀c3:C.(wf3 g c1 c3)→(wf3 g c c3)
             case clear_bind : b:B e:C u:T ⇒
                    assume g: G
                    assume c2: C
                    suppose H0: wf3 g (CHead e (Bind b) u) c2
                      consider H0
             case clear_flat : e:C c0:C :clear e c0 f:F u:T ⇒
                the thesis becomes ∀g:G.∀c2:C.∀H2:(wf3 g (CHead e (Flat f) u) c2).(wf3 g c0 c2)
                (H1) by induction hypothesis we know ∀g:G.∀c2:C.(wf3 g e c2)→(wf3 g c0 c2)
                    assume g: G
                    assume c2: C
                    suppose H2: wf3 g (CHead e (Flat f) u) c2
                      (H_y) by (wf3_gen_flat1 . . . . . H2) we proved wf3 g e c2
                      by (H1 . . H_y)
                      we proved wf3 g c0 c2
∀g:G.∀c2:C.∀H2:(wf3 g (CHead e (Flat f) u) c2).(wf3 g c0 c2)
          we proved ∀g:G.∀c3:C.(wf3 g c1 c3)→(wf3 g c c3)
       we proved ∀c1:C.∀c:C.(clear c1 c)→∀g:G.∀c3:C.(wf3 g c1 c3)→(wf3 g c c3)