ProofTab.gt.wcon2: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab
Lines 38-41 of bend-osdev-gf@0.1.1.0/proof_tab.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/proof_tab.bend&start_line=38&end_line=41

import Base

def 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)}:
  %ea : {WCon{a, x} == WCon{_, y} : Word(1n+p)}
  %ex : {WCon{a, x} == WCon{a, _} : Word(1n+p)}
  {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con