def u.le_refl

bend-osdev-u32@0.1.0.0 · PROOF_order.bend:307

import Base

307def u.le_refl(+a: U32) -> {ule(a, a) == True{} : Bool}:
308  %Equal.sym(Cmp, U32.cmp(a, a), EQ{}, u.refl(a)) : {Cmp.is_le(_) == True{} : Bool}
309  {==}