DEFINITION nf2_abst()
TYPE =
       ∀c:C
         .∀u:T
           .nf2 c u
             →∀b:B
                  .∀v:T
                    .∀t:T.(nf2 (CHead c (Bind b) v) t)→(nf2 c (THead (Bind Abst) u t))
BODY =
Show proof