def ud.dr

bend-osdev-u32@0.1.0.0 · PROOF.bend:1796

import Base

1796def ud.dr(G: Word(32n) & U32) -> {U32.to_nat(U32.mod.fin(G)) == ud.r(32n, G) : Nat}:
1797  match G:
1798    case (q, r):
1799      {==}