DEFINITION nf2_gen_void()
TYPE =
       ∀c:C.∀u:T.∀t:T.(nf2 c (THead (Bind Void) u (lift (S O) O t)))→∀P:Prop.P
BODY =
        assume c: C
        assume u: T
        assume t: T
          we must prove (nf2 c (THead (Bind Void) u (lift (S O) O t)))→∀P:Prop.P
          or equivalently 
                ∀t2:T
                    .pr2 c (THead (Bind Void) u (lift (S O) O t)) t2
                      →eq T (THead (Bind Void) u (lift (S O) O t)) t2
                  →∀P:Prop.P
           suppose H: 
              ∀t2:T
                .pr2 c (THead (Bind Void) u (lift (S O) O t)) t2
                  →eq T (THead (Bind Void) u (lift (S O) O t)) t2
           assume P: Prop
             (h1) 
                by (sym_not_eq . . . not_abst_void)
not (eq B Void Abst)
             end of h1
             (h2) by (pr0_refl .) we proved pr0 t t
             by (pr0_zeta . h1 . . h2 .)
             we proved pr0 (THead (Bind Void) u (lift (S O) O t)) t
             by (pr2_free . . . previous)
             we proved pr2 c (THead (Bind Void) u (lift (S O) O t)) t
             by (H . previous)
             we proved eq T (THead (Bind Void) u (lift (S O) O t)) t
             by (nf2_gen__nf2_gen_aux . . . . previous .)
             we proved P
          we proved 
             ∀t2:T
                 .pr2 c (THead (Bind Void) u (lift (S O) O t)) t2
                   →eq T (THead (Bind Void) u (lift (S O) O t)) t2
               →∀P:Prop.P
          that is equivalent to (nf2 c (THead (Bind Void) u (lift (S O) O t)))→∀P:Prop.P
       we proved 
          ∀c:C.∀u:T.∀t:T.(nf2 c (THead (Bind Void) u (lift (S O) O t)))→∀P:Prop.P