1	# Width transport changes the type index, never the stored bits.
2	import Base
3	
4	def transport(-source: Nat,-target: Nat,value: Word(source),width: {source == target : Nat}) -> Word(target):
5	  %width : Word(_)
6	  value
7	
8	law 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)}
16	
17	def transport_cons(source,target,bit,tail,width):
18	  %h@width : {transport(1n+source,1n+_,WCon{bit,tail},Equal.cong(Nat,Nat,n => 1n+n,source,_,h)) == WCon{bit,transport(source,_,tail,h)} : Word(1n+_)}
19	  {==}