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