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