ProofZb.app8: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_zb.bend as ProofZb
Lines 21-25 of lawful-words@0.1.0.0/proof_zb.bend: https://jend.leeeet.dev/read.txt?path=lawful-words@0.1.0.0/proof_zb.bend&start_line=21&end_line=25

import Base

# Eight bits x in front of r.
def app8(-n: Nat, x: Word(8n), r: Word(n)) -> Word(Nat.add(8n, n)):
  match x:
    case WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, WNil{}}}}}}}}}:
      WCon{c0, WCon{c1, WCon{c2, WCon{c3, WCon{c4, WCon{c5, WCon{c6, WCon{c7, r}}}}}}}}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  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=Base/base.bend&name=Word.Nil