DEFINITION wf3_total()
TYPE =
∀
g:
G
.
∀
c1:
C
.(
ex
C
λ
c2:
C
.
wf3
g c1 c2)
BODY =
Show proof