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