DEFINITION wf3_idem()
TYPE =
       ∀g:G.∀c1:C.∀c2:C.(wf3 g c1 c2)→(wf3 g c2 c2)
BODY =
Show proof