def un.wcon_eq

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

import Base

455def un.wcon_eq(-p: Nat, -x: Bool, -y: Bool, -s: Word(p), -t: Word(p), e1: {x == y : Bool}, e2: {s == t : Word(p)}) -> {WCon{x, s} == WCon{y, t} : Word(1n+p)}:
456  %e1 : {WCon{x, s} == WCon{_, t} : Word(1n+p)}
457  %e2 : {WCon{x, s} == WCon{x, _} : Word(1n+p)}
458  {==}