DEFINITION wf3_idem()
TYPE =
       ∀g:G.∀c1:C.∀c2:C.(wf3 g c1 c2)→(wf3 g c2 c2)
BODY =
        assume g: G
        assume c1: C
        assume c2: C
        suppose H: wf3 g c1 c2
          we proceed by induction on H to prove wf3 g c2 c2
             case wf3_sort : m:nat ⇒
                the thesis becomes wf3 g (CSort m) (CSort m)
                   by (wf3_sort . .)
wf3 g (CSort m) (CSort m)
             case wf3_bind : c3:C c4:C H0:wf3 g c3 c4 u:T t:T H2:ty3 g c3 u t b:B ⇒
                the thesis becomes wf3 g (CHead c4 (Bind b) u) (CHead c4 (Bind b) u)
                (H1) by induction hypothesis we know wf3 g c4 c4
                   by (wf3_ty3_conf . . . . H2 . H0)
                   we proved ty3 g c4 u t
                   by (wf3_bind . . . H1 . . previous .)
wf3 g (CHead c4 (Bind b) u) (CHead c4 (Bind b) u)
             case wf3_void : c3:C c4:C :wf3 g c3 c4 u:T :∀t:T.(ty3 g c3 u t)→False :B ⇒
                the thesis becomes 
                wf3
                  g
                  CHead c4 (Bind Void) (TSort O)
                  CHead c4 (Bind Void) (TSort O)
                (H1) by induction hypothesis we know wf3 g c4 c4
                   by (ty3_sort . . .)
                   we proved ty3 g c4 (TSort O) (TSort (next g O))
                   by (wf3_bind . . . H1 . . previous .)

                      wf3
                        g
                        CHead c4 (Bind Void) (TSort O)
                        CHead c4 (Bind Void) (TSort O)
             case wf3_flat : c3:C c4:C :wf3 g c3 c4 :T :F ⇒
                the thesis becomes the hypothesis H1
          we proved wf3 g c2 c2
       we proved ∀g:G.∀c1:C.∀c2:C.(wf3 g c1 c2)→(wf3 g c2 c2)