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