def AP.wcon_cong

bend-osdev-array@0.1.0.1 · PROOF.bend:318

import Base

318def AP.wcon_cong(-p: Nat, -b: Bool, -x: Word(p), -y: Word(p), e: {x == y : Word(p)}) -> {WCon{b, x} == WCon{b, y} : Word(1n+p)}:
319  %e : {WCon{b, x} == WCon{b, _} : Word(1n+p)}
320  {==}