DEFINITION cimp_flat_sx()
TYPE =
       ∀f:F.∀c:C.∀v:T.(cimp (CHead c (Flat f) v) c)
BODY =
Show proof