DEFINITION csubst1_flat()
TYPE =
       ∀f:F
         .∀i:nat
           .∀v:T
             .∀u1:T
               .∀u2:T
                 .subst1 i v u1 u2
                   →∀c1:C.∀c2:C.(csubst1 i v c1 c2)→(csubst1 i v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2))
BODY =
Show proof