def le_k

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32.bend:69

import Base

69def le_k(+k: Nat, +hk: {k == 32n : Nat}) -> {Nat.is_le(k, 32n) == True{} : Bool}:
70  %Equal.sym(Nat, k, 32n, hk) : {Nat.is_le(_, 32n) == True{} : Bool}
71  {==}