DEFINITION lt_blt()
TYPE =
       ∀x:nat.∀y:nat.(lt y x)→(eq bool (blt y x) true)
BODY =
Show proof