DEFINITION nf2_gen_flat()
TYPE =
       ∀f:F.∀c:C.∀u:T.∀t:T.(nf2 c (THead (Flat f) u t))→(land (nf2 c u) (nf2 c t))
BODY =
Show proof