DEFINITION sn3_gen_cflat()
TYPE =
       ∀f:F.∀c:C.∀u:T.∀t:T.(sn3 (CHead c (Flat f) u) t)→(sn3 c t)
BODY =
Show proof