def LeW

import minebender-game@1.0.0.0/proof_base.bend as ProofBase

import Base

656def LeW(+a: Nat, +b: Nat) -> Type:
657  Exists(Nat, k => {b == Nat.add(a, k) : Nat})

Uses (3)