DEFINITION nf2_gen_beta()
TYPE =
       ∀c:C
         .∀u:T
           .∀v:T
             .∀t:T
               .nf2 c (THead (Flat Appl) u (THead (Bind Abst) v t))
                 →∀P:Prop.P
BODY =
Show proof