DEFINITION getl_wf3_trans()
TYPE =
       ∀i:nat.∀c1:C.∀d1:C.(getl i c1 d1)→∀g:G.∀d2:C.(wf3 g d1 d2)→(ex2 C λc2:C.wf3 g c1 c2 λc2:C.getl i c2 d2)
BODY =
Show proof