DEFINITION wf3_getl_conf()
TYPE =
       ∀b:B
         .∀i:nat
           .∀c1:C
             .∀d1:C
               .∀v:T
                 .getl i c1 (CHead d1 (Bind b) v)
                   →∀g:G
                        .∀c2:C
                          .wf3 g c1 c2
                            →∀w:T.(ty3 g d1 v w)→(ex2 C λd2:C.getl i c2 (CHead d2 (Bind b) v) λd2:C.wf3 g d1 d2)
BODY =
Show proof