WordWidth.transport_cons: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_width.bend as WordWidth
Lines 8-15 of stelliferous@0.0.2.0/proofs/word_width.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_width.bend&start_line=8&end_line=15

import Base

law transport_cons:
  for +source: Nat
  for +target: Nat
  for +bit: Bool
  for +tail: Word(source)
  for width: {source == target : Nat}
  {transport(1n+source,1n+target,WCon{bit,tail},Equal.cong(Nat,Nat,n => 1n+n,source,target,width)) == WCon{bit,transport(source,target,tail,
        width)} : Word(1n+target)}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_width.bend&name=transport