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