DEFINITION nf2_gen__nf2_gen_aux()
TYPE =
       ∀b:B
         .∀x:T
           .∀u:T.∀d:nat.(eq T (THead (Bind b) u (lift (S O) d x)) x)→∀P:Prop.P
BODY =
Show proof