law recover

stelliferous@0.0.2.0 · proofs/word_encoding.bend:178

import Base

178law recover:
179  for +n: Nat
180  for +m: Nat
181  for +w: Word(Nat.add(n,m))
182  {join(n,m,split(n,m,w)) == w : Word(Nat.add(n,m))}