DEFINITION wcpr0_getl_back()
TYPE =
       ∀c1:C
         .∀c2:C
           .wcpr0 c2 c1
             →∀h:nat
                  .∀e1:C
                    .∀u1:T
                      .∀k:K
                        .getl h c1 (CHead e1 k u1)
                          →ex3_2 C T λe2:C.λu2:T.getl h c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e2 e1 λ:C.λu2:T.pr0 u2 u1
BODY =
Show proof