def un.wcon_cong

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

import Base

580def un.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)}:
581  %e : {WCon{s, x} == WCon{s, _} : Word(1n+p)}
582  {==}