def ws.wcon_cong

bend-osdev-word64@0.1.1.0 · proof_shift.bend:252

import Base

252def ws.wcon_cong(-p: Nat, -s: Bool, -x: Word(p), -y: Word(p), e: {x == y : Word(p)}) -> {WCon{s, x} == WCon{s, y} : Word(1n+p)}:
253  %e : {WCon{s, x} == WCon{s, _} : Word(1n+p)}
254  {==}