def u.lt_irrefl

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

import Base

320def u.lt_irrefl(+a: U32, +e: {ult(a, a) == True{} : Bool}) -> Empty:
321  ab.lt_eqc(U32.cmp(a, a), u.refl(a), e)