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