DEFINITION nf2_gen_cast()
TYPE =
       ∀c:C.∀u:T.∀t:T.(nf2 c (THead (Flat Cast) u t))→∀P:Prop.P
BODY =
        assume c: C
        assume u: T
        assume t: T
        suppose H: nf2 c (THead (Flat Cast) u t)
        assume P: Prop
          by (pr0_refl .)
          we proved pr0 t t
          by (pr0_tau . . previous .)
          we proved pr0 (THead (Flat Cast) u t) t
          by (pr2_free . . . previous)
          we proved pr2 c (THead (Flat Cast) u t) t
          by (H . previous)
          we proved eq T (THead (Flat Cast) u t) t
          by (thead_x_y_y . . . previous .)
          we proved P
       we proved ∀c:C.∀u:T.∀t:T.(nf2 c (THead (Flat Cast) u t))→∀P:Prop.P