DEFINITION aprem_repl()
TYPE =
       ∀g:G
         .∀a1:A.∀a2:A.(leq g a1 a2)→∀i:nat.∀b2:A.(aprem i a2 b2)→(ex2 A λb1:A.leq g b1 b2 λb1:A.aprem i a1 b1)
BODY =
Show proof