DEFINITION getl_conf_le()
TYPE =
       ∀i:nat
         .∀a:C
           .∀c:C
             .getl i c a
               →∀e:C.∀h:nat.(getl h c e)→(le h i)→(getl (minus i h) e a)
BODY =
Show proof