law join_prepend

stelliferous@0.0.2.0 · proofs/word_encoding.bend:167

import Base

167law join_prepend:
168  for +n: Nat
169  for +m: Nat
170  for +b: Bool
171  for +parts: Split<n,m>
172  {WCon{b,join(n,m,parts)} == join(1n+n,m,prepend(n,m,b,parts)) : Word(1n+Nat.add(n,m))}