DEFINITION clear_wf3_trans()
TYPE =
       ∀c1:C.∀d1:C.(clear c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.clear c2 d2)
BODY =
Show proof