law transport_cons

stelliferous@0.0.2.0 · proofs/word_width.bend:8

import Base

8law transport_cons:
9  for +source: Nat
10  for +target: Nat
11  for +bit: Bool
12  for +tail: Word(source)
13  for width: {source == target : Nat}
14  {transport(1n+source,1n+target,WCon{bit,tail},Equal.cong(Nat,Nat,n => 1n+n,source,target,width)) == WCon{bit,transport(source,target,tail,
15        width)} : Word(1n+target)}