DEFINITION wf3_gen_flat1()
TYPE =
       ∀g:G.∀c1:C.∀x:C.∀v:T.∀f:F.(wf3 g (CHead c1 (Flat f) v) x)→(wf3 g c1 x)
BODY =
Show proof