DEFINITION llt_repl()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→∀a3:A.(llt a1 a3)→(llt a2 a3)
BODY =
Show proof