DEFINITION wf3_gen_sort1()
TYPE =
       ∀g:G.∀x:C.∀m:nat.(wf3 g (CSort m) x)→(eq C x (CSort m))
BODY =
Show proof