def gt.wcon2

bend-osdev-gf@0.1.1.0 · proof_tab.bend:38

import Base

38def gt.wcon2(-p: Nat, -a: Bool, -b: Bool, -x: Word(p), -y: Word(p), ea: {a == b : Bool}, ex: {x == y : Word(p)}) -> {WCon{a, x} == WCon{b, y} : Word(1n+p)}:
39  %ea : {WCon{a, x} == WCon{_, y} : Word(1n+p)}
40  %ex : {WCon{a, x} == WCon{a, _} : Word(1n+p)}
41  {==}