def u32_eq_self

bend-osdev-bytes@0.1.1.0 · PROOF.bend:376

import Base
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

376def u32_eq_self(a: U32) -> {U32.is_eq(a, a) == True{} : Bool}:
377  match a:
378    case U32{+w}:
379      %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, UO.word_cmp_refl(32n, w)) : {Cmp.is_eq(_) == True{} : Bool}
380      {==}