DEFINITION nf2_gen_abst()
TYPE =
       ∀c:C
         .∀u:T
           .∀t:T
             .nf2 c (THead (Bind Abst) u t)
               →land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)
BODY =
Show proof