1	import Base
2	import bend-osdev-word64@0.1.1.0/word64.bend as W
3	import bend-osdev-word64@0.1.1.0/LAWS.bend as WL
4	import bend-osdev-word64@0.1.1.0/PROOF.bend as WP
5	import ./bytes.bend as B
6	import ./LAWS.bend as Laws
7	import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
8	import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO
9	import bend-osdev-u32@0.1.0.0/PROOF.bend as UP
10	import bend-osdev-u32@0.1.0.0/PROOF_order.bend as UOP
11	
12	def Laws.le16_round_trip(v):
13	  match v:
14	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
15	      {==}
16	
17	def Laws.be16_round_trip(v):
18	  match v:
19	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
20	      {==}
21	
22	def Laws.le32_round_trip(v):
23	  match v:
24	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
25	      {==}
26	
27	def Laws.be32_round_trip(v):
28	  match v:
29	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
30	      {==}
31	
32	# Reading a 32-bit field at the head of a longer string, and skipping it
33	def le32_head_app(x: U32, r: List<&2, U32>) -> {B.le32.head(B.append(B.le32(x), r)) == Some{x} : Maybe<&2, U32>}:
34	  match x:
35	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
36	      {==}
37	
38	def be32_head_app(x: U32, r: List<&2, U32>) -> {B.be32.head(B.append(B.be32(x), r)) == Some{x} : Maybe<&2, U32>}:
39	  match x:
40	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
41	      {==}
42	
43	def drop4_le32(x: U32, r: List<&2, U32>) -> {B.drop(4n, B.append(B.le32(x), r)) == r : List<&2, U32>}:
44	  match x:
45	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
46	      {==}
47	
48	def drop4_be32(x: U32, r: List<&2, U32>) -> {B.drop(4n, B.append(B.be32(x), r)) == r : List<&2, U32>}:
49	  match x:
50	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
51	      {==}
52	
53	def Laws.le64_round_trip(v):
54	  %Equal.sym(Maybe<&2, U32>, B.le32_at(B.le64(v), 0n), Some{W.W64.lo(v)}, le32_head_app(W.W64.lo(v), B.le32(W.W64.hi(v)))) : {B.le64.join(_, B.le32_at(B.le64(v), 4n)) == Some{v} : Maybe<&2, W.W64>}
55	  %Equal.sym(Maybe<&2, U32>, B.le32_at(B.le64(v), 4n), Some{W.W64.hi(v)}, Equal.trans(Maybe<&2, U32>, B.le32_at(B.le64(v), 4n), B.le32.head(B.le32(W.W64.hi(v))), Some{W.W64.hi(v)}, Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.le32.head(l), B.drop(4n, B.le64(v)), B.le32(W.W64.hi(v)), drop4_le32(W.W64.lo(v), B.le32(W.W64.hi(v)))), Laws.le32_round_trip(W.W64.hi(v)))) : {B.le64.join(Some{W.W64.lo(v)}, _) == Some{v} : Maybe<&2, W.W64>}
56	  %WL.parts_of(v) : {Some{W.W64.from_parts(W.W64.hi(v), W.W64.lo(v))} == Some{_} : Maybe<&2, W.W64>}
57	  {==}
58	
59	def Laws.be64_round_trip(v):
60	  %Equal.sym(Maybe<&2, U32>, B.be32_at(B.be64(v), 0n), Some{W.W64.hi(v)}, be32_head_app(W.W64.hi(v), B.be32(W.W64.lo(v)))) : {B.le64.join(B.be32_at(B.be64(v), 4n), _) == Some{v} : Maybe<&2, W.W64>}
61	  %Equal.sym(Maybe<&2, U32>, B.be32_at(B.be64(v), 4n), Some{W.W64.lo(v)}, Equal.trans(Maybe<&2, U32>, B.be32_at(B.be64(v), 4n), B.be32.head(B.be32(W.W64.lo(v))), Some{W.W64.lo(v)}, Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.be32.head(l), B.drop(4n, B.be64(v)), B.be32(W.W64.lo(v)), drop4_be32(W.W64.hi(v), B.be32(W.W64.lo(v)))), Laws.be32_round_trip(W.W64.lo(v)))) : {B.le64.join(_, Some{W.W64.hi(v)}) == Some{v} : Maybe<&2, W.W64>}
62	  %WL.parts_of(v) : {Some{W.W64.from_parts(W.W64.hi(v), W.W64.lo(v))} == Some{_} : Maybe<&2, W.W64>}
63	  {==}
64	
65	def Laws.byte_below_256(b):
66	  match b:
67	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
68	      {==}
69	
70	def Laws.take_drop(n, xs):
71	  match n xs:
72	    case 0n _:
73	      {==}
74	    case 1n+p Nil{}:
75	      {==}
76	    case 1n+p Con{h, t}:
77	      %Laws.take_drop(p, t) : {Con{h, B.append(B.take(p, t), B.drop(p, t))} == Con{h, _} : List<&2, U32>}
78	      {==}
79	
80	def Laws.be32_order():
81	  {==}
82	
83	def Laws.le32_order():
84	  {==}
85	
86	def Laws.be64_order():
87	  {==}
88	
89	def Laws.le16_at_offset():
90	  {==}
91	
92	def Laws.short_input():
93	  {==}
94	
95	def Laws.at_end():
96	  {==}
97	
98	def Laws.masks_elements():
99	  {==}
100	
101	def Laws.hex_text():
102	  {==}
103	
104	def Laws.octets_le16_round_trip(v):
105	  match v:
106	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
107	      {==}
108	
109	def Laws.octets_be16_round_trip(v):
110	  match v:
111	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
112	      {==}
113	
114	def Laws.octets_le32_round_trip(v):
115	  match v:
116	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
117	      {==}
118	
119	def Laws.octets_be32_round_trip(v):
120	  match v:
121	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
122	      {==}
123	
124	# the eight bytes of two le32 fields come back unchanged through Octets
125	def field64_le(x: U32, y: U32) -> {B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.append(B.le32(x), B.le32(y))))) == B.append(B.le32(x), B.le32(y)) : List<&2, U32>}:
126	  match x y:
127	    case U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, WCon{x16, WCon{x17, WCon{x18, WCon{x19, WCon{x20, WCon{x21, WCon{x22, WCon{x23, WCon{x24, WCon{x25, WCon{x26, WCon{x27, WCon{x28, WCon{x29, WCon{x30, WCon{x31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
128	      {==}
129	
130	# the eight bytes of two be32 fields come back unchanged through Octets
131	def field64_be(x: U32, y: U32) -> {B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.append(B.be32(x), B.be32(y))))) == B.append(B.be32(x), B.be32(y)) : List<&2, U32>}:
132	  match x y:
133	    case U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, WCon{x16, WCon{x17, WCon{x18, WCon{x19, WCon{x20, WCon{x21, WCon{x22, WCon{x23, WCon{x24, WCon{x25, WCon{x26, WCon{x27, WCon{x28, WCon{x29, WCon{x30, WCon{x31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
134	      {==}
135	
136	def Laws.octets_le64_round_trip(v):
137	  %Equal.sym(List<&2, U32>, B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.le64(v)))), B.le64(v), field64_le(W.W64.lo(v), W.W64.hi(v))) : {B.le64_at(_, 0n) == Some{v} : Maybe<&2, W.W64>}
138	  Laws.le64_round_trip(v)
139	
140	def Laws.octets_be64_round_trip(v):
141	  %Equal.sym(List<&2, U32>, B.w8s.to_list.fast(B.w8s.take.fast(8n, B.w8s.of_list.fast(B.be64(v)))), B.be64(v), field64_be(W.W64.hi(v), W.W64.lo(v))) : {B.be64_at(_, 0n) == Some{v} : Maybe<&2, W.W64>}
142	  Laws.be64_round_trip(v)
143	
144	# Word lists: the lemmas the Octets laws are built from
145	
146	def bits8_of_bits8(w: B.OctByte) -> {B.oct.of(B.oct.to(w)) == w : B.OctByte}:
147	  match w:
148	    case B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}:
149	      {==}
150	
151	def w8s_of_to(ws: List<&2, B.OctByte>) -> {B.w8s.of_list(B.w8s.to_list(ws)) == ws : List<&2, B.OctByte>}:
152	  match ws:
153	    case Nil{}:
154	      {==}
155	    case Con{h, t}:
156	      %bits8_of_bits8(h) : {Con{B.oct.of(B.oct.to(h)), B.w8s.of_list(B.w8s.to_list(t))} == Con{_, t} : List<&2, B.OctByte>}
157	      %w8s_of_to(t) : {Con{B.oct.of(B.oct.to(h)), B.w8s.of_list(B.w8s.to_list(t))} == Con{B.oct.of(B.oct.to(h)), _} : List<&2, B.OctByte>}
158	      {==}
159	
160	# a word through one OctByte and back is its byte
161	def oct_byte(h: U32) -> {B.oct.to(B.oct.of(h)) == B.byte(h) : U32}:
162	  match h:
163	    case U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
164	      {==}
165	
166	def w8s_to_of(xs: List<&2, U32>) -> {B.w8s.to_list(B.w8s.of_list(xs)) == B.mask(xs) : List<&2, U32>}:
167	  match xs:
168	    case Nil{}:
169	      {==}
170	    case Con{h, t}:
171	      %w8s_to_of(t) : {Con{B.oct.to(B.oct.of(h)), B.w8s.to_list(B.w8s.of_list(t))} == Con{B.byte(h), _} : List<&2, U32>}
172	      %oct_byte(h) : {Con{B.oct.to(B.oct.of(h)), B.w8s.to_list(B.w8s.of_list(t))} == Con{_, B.w8s.to_list(B.w8s.of_list(t))} : List<&2, U32>}
173	      {==}
174	
175	def w8s_to_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.to_list(List.append(&2, B.OctByte, xs, ys)) == B.append(B.w8s.to_list(xs), B.w8s.to_list(ys)) : List<&2, U32>}:
176	  match xs:
177	    case Nil{}:
178	      {==}
179	    case Con{h, t}:
180	      %w8s_to_app(t, ys) : {Con{B.oct.to(h), B.w8s.to_list(List.append(&2, B.OctByte, t, ys))} == Con{B.oct.to(h), _} : List<&2, U32>}
181	      {==}
182	
183	def w8s_len(ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, ws) == List.length(&2, U32, B.w8s.to_list(ws)) : Nat}:
184	  match ws:
185	    case Nil{}:
186	      {==}
187	    case Con{h, t}:
188	      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, t), List.length(&2, U32, B.w8s.to_list(t)), w8s_len(t))
189	
190	def w8s_take_drop(n: Nat, ws: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, B.w8s.take(n, ws), B.w8s.drop(n, ws)) == ws : List<&2, B.OctByte>}:
191	  match n ws:
192	    case 0n _:
193	      {==}
194	    case 1n+p Nil{}:
195	      {==}
196	    case 1n+p Con{h, t}:
197	      %w8s_take_drop(p, t) : {Con{h, List.append(&2, B.OctByte, B.w8s.take(p, t), B.w8s.drop(p, t))} == Con{h, _} : List<&2, B.OctByte>}
198	      {==}
199	
200	def w8s_take_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)) == xs : List<&2, B.OctByte>}:
201	  match xs:
202	    case Nil{}:
203	      {==}
204	    case Con{h, t}:
205	      %w8s_take_app(t, ys) : {Con{h, B.w8s.take(List.length(&2, B.OctByte, t), List.append(&2, B.OctByte, t, ys))} == Con{h, _} : List<&2, B.OctByte>}
206	      {==}
207	
208	def w8s_drop_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)) == ys : List<&2, B.OctByte>}:
209	  match xs:
210	    case Nil{}:
211	      {==}
212	    case Con{h, t}:
213	      w8s_drop_app(t, ys)
214	
215	def w8s_len_app(xs: List<&2, B.OctByte>, ys: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)) == Nat.add(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys)) : Nat}:
216	  match xs:
217	    case Nil{}:
218	      {==}
219	    case Con{h, t}:
220	      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, List.append(&2, B.OctByte, t, ys)), Nat.add(List.length(&2, B.OctByte, t), List.length(&2, B.OctByte, ys)), w8s_len_app(t, ys))
221	
222	# Fast forms equal structural forms, for every input. bytes.bend's Octets
223	# runs the tail-recursive *.fast defs; these lemmas (each stated
224	# ref == fast, the direction rewrites use) carry every law proved about the
225	# structural defs over to them.
226	
227	def r8_rr(ws: List<&2, B.OctByte>, acc: List<&2, B.OctByte>, b: List<&2, B.OctByte>) -> {B.w8s.rev_onto(B.w8s.rev_onto(ws, acc), b) == B.w8s.rev_onto(acc, List.append(&2, B.OctByte, ws, b)) : List<&2, B.OctByte>}:
228	  match ws:
229	    case Nil{}:
230	      {==}
231	    case Con{h, t}:
232	      r8_rr(t, Con{h, acc}, b)
233	
234	def ru_rr(xs: List<&2, U32>, acc: List<&2, U32>, b: List<&2, U32>) -> {B.rev_onto(B.rev_onto(xs, acc), b) == B.rev_onto(acc, List.append(&2, U32, xs, b)) : List<&2, U32>}:
235	  match xs:
236	    case Nil{}:
237	      {==}
238	    case Con{h, t}:
239	      ru_rr(t, Con{h, acc}, b)
240	
241	def app_nil8(+ws: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, ws, Nil{}) == ws : List<&2, B.OctByte>}:
242	  match ws:
243	    case Nil{}:
244	      {==}
245	    case Con{h, t}:
246	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, List.append(&2, B.OctByte, t, Nil{}), t, app_nil8(t))
247	
248	def app_nilu(+xs: List<&2, U32>) -> {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}:
249	  match xs:
250	    case Nil{}:
251	      {==}
252	    case Con{h, t}:
253	      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{h, l}, List.append(&2, U32, t, Nil{}), t, app_nilu(t))
254	
255	def g_of(xs: List<&2, U32>, acc: List<&2, B.OctByte>) -> {B.w8s.of_list.go(xs, acc) == B.w8s.rev_onto(B.w8s.of_list(xs), acc) : List<&2, B.OctByte>}:
256	  match xs:
257	    case Nil{}:
258	      {==}
259	    case Con{h, t}:
260	      g_of(t, Con{B.oct.of(h), acc})
261	
262	def F_of(+xs: List<&2, U32>) -> {B.w8s.of_list(xs) == B.w8s.of_list.fast(xs) : List<&2, B.OctByte>}:
263	  Equal.sym(List<&2, B.OctByte>, B.w8s.of_list.fast(xs), B.w8s.of_list(xs),
264	    Equal.trans(List<&2, B.OctByte>, B.w8s.of_list.fast(xs), B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.of_list(xs), Nil{}), Nil{}), B.w8s.of_list(xs),
265	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => B.w8s.rev_onto(l, Nil{}), B.w8s.of_list.go(xs, Nil{}), B.w8s.rev_onto(B.w8s.of_list(xs), Nil{}), g_of(xs, Nil{})),
266	      Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.of_list(xs), Nil{}), Nil{}), List.append(&2, B.OctByte, B.w8s.of_list(xs), Nil{}), B.w8s.of_list(xs),
267	        r8_rr(B.w8s.of_list(xs), Nil{}, Nil{}), app_nil8(B.w8s.of_list(xs)))))
268	
269	def g_to(ws: List<&2, B.OctByte>, acc: List<&2, U32>) -> {B.w8s.to_list.go(ws, acc) == B.rev_onto(B.w8s.to_list(ws), acc) : List<&2, U32>}:
270	  match ws:
271	    case Nil{}:
272	      {==}
273	    case Con{h, t}:
274	      g_to(t, Con{B.oct.to(h), acc})
275	
276	def F_to(+ws: List<&2, B.OctByte>) -> {B.w8s.to_list(ws) == B.w8s.to_list.fast(ws) : List<&2, U32>}:
277	  Equal.sym(List<&2, U32>, B.w8s.to_list.fast(ws), B.w8s.to_list(ws),
278	    Equal.trans(List<&2, U32>, B.w8s.to_list.fast(ws), B.rev_onto(B.rev_onto(B.w8s.to_list(ws), Nil{}), Nil{}), B.w8s.to_list(ws),
279	      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.w8s.to_list.go(ws, Nil{}), B.rev_onto(B.w8s.to_list(ws), Nil{}), g_to(ws, Nil{})),
280	      Equal.trans(List<&2, U32>, B.rev_onto(B.rev_onto(B.w8s.to_list(ws), Nil{}), Nil{}), List.append(&2, U32, B.w8s.to_list(ws), Nil{}), B.w8s.to_list(ws),
281	        ru_rr(B.w8s.to_list(ws), Nil{}, Nil{}), app_nilu(B.w8s.to_list(ws)))))
282	
283	def g_take(n: Nat, ws: List<&2, B.OctByte>, acc: List<&2, B.OctByte>) -> {B.w8s.take.go(n, ws, acc) == B.w8s.rev_onto(B.w8s.take(n, ws), acc) : List<&2, B.OctByte>}:
284	  match n ws:
285	    case 0n _:
286	      {==}
287	    case 1n+p Nil{}:
288	      {==}
289	    case 1n+p Con{h, t}:
290	      g_take(p, t, Con{h, acc})
291	
292	def F_take(+n: Nat, +ws: List<&2, B.OctByte>) -> {B.w8s.take(n, ws) == B.w8s.take.fast(n, ws) : List<&2, B.OctByte>}:
293	  Equal.sym(List<&2, B.OctByte>, B.w8s.take.fast(n, ws), B.w8s.take(n, ws),
294	    Equal.trans(List<&2, B.OctByte>, B.w8s.take.fast(n, ws), B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.take(n, ws), Nil{}), Nil{}), B.w8s.take(n, ws),
295	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => B.w8s.rev_onto(l, Nil{}), B.w8s.take.go(n, ws, Nil{}), B.w8s.rev_onto(B.w8s.take(n, ws), Nil{}), g_take(n, ws, Nil{})),
296	      Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.rev_onto(B.w8s.take(n, ws), Nil{}), Nil{}), List.append(&2, B.OctByte, B.w8s.take(n, ws), Nil{}), B.w8s.take(n, ws),
297	        r8_rr(B.w8s.take(n, ws), Nil{}, Nil{}), app_nil8(B.w8s.take(n, ws)))))
298	
299	def F_app(+xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, xs, ys) == B.w8s.append.fast(xs, ys) : List<&2, B.OctByte>}:
300	  Equal.sym(List<&2, B.OctByte>, B.w8s.append.fast(xs, ys), List.append(&2, B.OctByte, xs, ys), r8_rr(xs, Nil{}, ys))
301	
302	def g_len(+ws: List<&2, B.OctByte>, +n: Nat) -> {B.w8s.len.go(ws, n) == Nat.add(List.length(&2, B.OctByte, ws), n) : Nat}:
303	  match ws:
304	    case Nil{}:
305	      {==}
306	    case Con{h, t}:
307	      Equal.trans(Nat, B.w8s.len.go(t, 1n+n), Nat.add(List.length(&2, B.OctByte, t), 1n+n), 1n+Nat.add(List.length(&2, B.OctByte, t), n),
308	        g_len(t, 1n+n), UL.nat_add_succ(List.length(&2, B.OctByte, t), n))
309	
310	def F_len(+ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, ws) == B.w8s.len.fast(ws) : Nat}:
311	  Equal.sym(Nat, B.w8s.len.fast(ws), List.length(&2, B.OctByte, ws),
312	    Equal.trans(Nat, B.w8s.len.go(ws, 0n), Nat.add(List.length(&2, B.OctByte, ws), 0n), List.length(&2, B.OctByte, ws),
313	      g_len(ws, 0n), UL.nat_add_zero(List.length(&2, B.OctByte, ws))))
314	
315	def zeros_cons(+p: Nat, +acc: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, B.w8s.zeros(p), Con{B.oct.zero(), acc}) == Con{B.oct.zero(), List.append(&2, B.OctByte, B.w8s.zeros(p), acc)} : List<&2, B.OctByte>}:
316	  match p:
317	    case 0n:
318	      {==}
319	    case 1n+q:
320	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{B.oct.zero(), l}, List.append(&2, B.OctByte, B.w8s.zeros(q), Con{B.oct.zero(), acc}), Con{B.oct.zero(), List.append(&2, B.OctByte, B.w8s.zeros(q), acc)}, zeros_cons(q, acc))
321	
322	def g_zeros(+n: Nat, +acc: List<&2, B.OctByte>) -> {B.w8s.zeros.go(n, acc) == List.append(&2, B.OctByte, B.w8s.zeros(n), acc) : List<&2, B.OctByte>}:
323	  match n:
324	    case 0n:
325	      {==}
326	    case 1n+p:
327	      Equal.trans(List<&2, B.OctByte>, B.w8s.zeros.go(p, Con{B.oct.zero(), acc}), List.append(&2, B.OctByte, B.w8s.zeros(p), Con{B.oct.zero(), acc}), Con{B.oct.zero(), List.append(&2, B.OctByte, B.w8s.zeros(p), acc)},
328	        g_zeros(p, Con{B.oct.zero(), acc}), zeros_cons(p, acc))
329	
330	def F_zeros(+n: Nat) -> {B.w8s.zeros(n) == B.w8s.zeros.fast(n) : List<&2, B.OctByte>}:
331	  Equal.sym(List<&2, B.OctByte>, B.w8s.zeros.fast(n), B.w8s.zeros(n),
332	    Equal.trans(List<&2, B.OctByte>, B.w8s.zeros.go(n, Nil{}), List.append(&2, B.OctByte, B.w8s.zeros(n), Nil{}), B.w8s.zeros(n),
333	      g_zeros(n, Nil{}), app_nil8(B.w8s.zeros(n))))
334	
335	def w8s_zeros_list(+n: Nat) -> {B.w8s.to_list(B.w8s.zeros(n)) == B.zeros(n) : List<&2, U32>}:
336	  match n:
337	    case 0n:
338	      {==}
339	    case 1n+p:
340	      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{0, l}, B.w8s.to_list(B.w8s.zeros(p)), B.zeros(p), w8s_zeros_list(p))
341	
342	# The Octets laws: each rewrites Octets' fast forms to the structural ones,
343	# then uses the word-list lemmas
344	
345	def p_octets_take_drop(+n: Nat, +o: B.Octets) -> {B.Octets.append(B.Octets.take(n, o), B.Octets.drop(n, o)) == o : B.Octets}:
346	  match o:
347	    case B.Octets{+ws}:
348	      %F_app(B.w8s.take.fast(n, ws), B.w8s.drop(n, ws)) : {B.Octets{_} == B.Octets{ws} : B.Octets}
349	      %F_take(n, ws) : {B.Octets{List.append(&2, B.OctByte, _, B.w8s.drop(n, ws))} == B.Octets{ws} : B.Octets}
350	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, List.append(&2, B.OctByte, B.w8s.take(n, ws), B.w8s.drop(n, ws)), ws, w8s_take_drop(n, ws))
351	
352	def Laws.octets_take_drop(n, o):
353	  p_octets_take_drop(n, o)
354	
355	def p_octets_of_to(+o: B.Octets) -> {B.Octets.of_list(B.Octets.to_list(o)) == o : B.Octets}:
356	  match o:
357	    case B.Octets{+ws}:
358	      %F_of(B.w8s.to_list.fast(ws)) : {B.Octets{_} == B.Octets{ws} : B.Octets}
359	      %F_to(ws) : {B.Octets{B.w8s.of_list(_)} == B.Octets{ws} : B.Octets}
360	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.of_list(B.w8s.to_list(ws)), ws, w8s_of_to(ws))
361	
362	def Laws.octets_of_to(o):
363	  p_octets_of_to(o)
364	
365	def p_octets_to_of(+xs: List<&2, U32>) -> {B.Octets.to_list(B.Octets.of_list(xs)) == B.mask(xs) : List<&2, U32>}:
366	  %F_to(B.w8s.of_list.fast(xs)) : {_ == B.mask(xs) : List<&2, U32>}
367	  %F_of(xs) : {B.w8s.to_list(_) == B.mask(xs) : List<&2, U32>}
368	  w8s_to_of(xs)
369	
370	def Laws.octets_to_of(xs):
371	  p_octets_to_of(xs)
372	
373	def Laws.octets_of_list_idempotent(xs):
374	  Laws.octets_of_to(B.Octets.of_list(xs))
375	
376	def u32_eq_self(a: U32) -> {U32.is_eq(a, a) == True{} : Bool}:
377	  match a:
378	    case U32{+w}:
379	      %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, UO.word_cmp_refl(32n, w)) : {Cmp.is_eq(_) == True{} : Bool}
380	      {==}
381	
382	def list_eq_self(xs: List<&2, U32>) -> {B.list_eq(xs, xs) == True{} : Bool}:
383	  match xs:
384	    case Nil{}:
385	      {==}
386	    case Con{+h, +t}:
387	      %Equal.sym(Bool, U32.is_eq(h, h), True{}, u32_eq_self(h)) : {Bool.and(_, B.list_eq(t, t)) == True{} : Bool}
388	      list_eq_self(t)
389	
390	def w8s_eq_self(ws: List<&2, B.OctByte>) -> {B.w8s.eq(ws, ws, True{}) == True{} : Bool}:
391	  match ws:
392	    case Nil{}:
393	      {==}
394	    case Con{+h, +t}:
395	      %Equal.sym(Bool, U32.is_eq(B.oct.to(h), B.oct.to(h)), True{}, u32_eq_self(B.oct.to(h))) : {B.w8s.eq(t, t, Bool.and(True{}, _)) == True{} : Bool}
396	      w8s_eq_self(t)
397	
398	def Laws.octets_is_eq_refl(o):
399	  match o:
400	    case B.Octets{+ws}:
401	      w8s_eq_self(ws)
402	
403	def Laws.octets_masks():
404	  {==}
405	
406	def Laws.octets_slice():
407	  {==}
408	
409	def p_octets_append_list(+a: B.Octets, +b: B.Octets) -> {B.Octets.to_list(B.Octets.append(a, b)) == B.append(B.Octets.to_list(a), B.Octets.to_list(b)) : List<&2, U32>}:
410	  match a b:
411	    case B.Octets{+xs} B.Octets{+ys}:
412	      %F_to(B.w8s.append.fast(xs, ys)) : {_ == B.append(B.w8s.to_list.fast(xs), B.w8s.to_list.fast(ys)) : List<&2, U32>}
413	      %F_app(xs, ys) : {B.w8s.to_list(_) == B.append(B.w8s.to_list.fast(xs), B.w8s.to_list.fast(ys)) : List<&2, U32>}
414	      %F_to(xs) : {B.w8s.to_list(List.append(&2, B.OctByte, xs, ys)) == B.append(_, B.w8s.to_list.fast(ys)) : List<&2, U32>}
415	      %F_to(ys) : {B.w8s.to_list(List.append(&2, B.OctByte, xs, ys)) == B.append(B.w8s.to_list(xs), _) : List<&2, U32>}
416	      w8s_to_app(xs, ys)
417	
418	def Laws.octets_append_list(a, b):
419	  p_octets_append_list(a, b)
420	
421	def p_octets_len_list(+o: B.Octets) -> {B.Octets.len(o) == B.len(B.Octets.to_list(o)) : Nat}:
422	  match o:
423	    case B.Octets{+ws}:
424	      %F_len(ws) : {_ == B.len(B.w8s.to_list.fast(ws)) : Nat}
425	      %F_to(ws) : {List.length(&2, B.OctByte, ws) == B.len(_) : Nat}
426	      w8s_len(ws)
427	
428	def Laws.octets_len_list(o):
429	  p_octets_len_list(o)
430	
431	def p_octets_take_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.take(B.Octets.len(a), B.Octets.append(a, b)) == a : B.Octets}:
432	  match a b:
433	    case B.Octets{+xs} B.Octets{+ys}:
434	      %F_take(B.w8s.len.fast(xs), B.w8s.append.fast(xs, ys)) : {B.Octets{_} == B.Octets{xs} : B.Octets}
435	      %F_len(xs) : {B.Octets{B.w8s.take(_, B.w8s.append.fast(xs, ys))} == B.Octets{xs} : B.Octets}
436	      %F_app(xs, ys) : {B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), _)} == B.Octets{xs} : B.Octets}
437	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)), xs, w8s_take_app(xs, ys))
438	
439	def Laws.octets_take_append(a, b):
440	  p_octets_take_append(a, b)
441	
442	def p_octets_drop_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.drop(B.Octets.len(a), B.Octets.append(a, b)) == b : B.Octets}:
443	  match a b:
444	    case B.Octets{+xs} B.Octets{+ys}:
445	      %F_len(xs) : {B.Octets{B.w8s.drop(_, B.w8s.append.fast(xs, ys))} == B.Octets{ys} : B.Octets}
446	      %F_app(xs, ys) : {B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), _)} == B.Octets{ys} : B.Octets}
447	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)), ys, w8s_drop_app(xs, ys))
448	
449	def Laws.octets_drop_append(a, b):
450	  p_octets_drop_append(a, b)
451	
452	def p_octets_split_at_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.split_at(B.Octets.len(a), B.Octets.append(a, b)) == Some{B.OctetsSplit{a, b}} : Maybe<&2, B.OctetsSplit>}:
453	  match a b:
454	    case B.Octets{+xs} B.Octets{+ys}:
455	      %F_app(xs, ys) : {B.Octets.split_at.pick(Nat.is_le(B.w8s.len.fast(xs), B.w8s.len.fast(_)), B.w8s.len.fast(xs), B.Octets{B.w8s.append.fast(xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
456	      %F_app(xs, ys) : {B.Octets.split_at.pick(Nat.is_le(B.w8s.len.fast(xs), B.w8s.len.fast(List.append(&2, B.OctByte, xs, ys))), B.w8s.len.fast(xs), B.Octets{_}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
457	      %F_len(List.append(&2, B.OctByte, xs, ys)) : {B.Octets.split_at.pick(Nat.is_le(B.w8s.len.fast(xs), _), B.w8s.len.fast(xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
458	      %F_len(xs) : {B.Octets.split_at.pick(Nat.is_le(_, List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys))), B.w8s.len.fast(xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
459	      %F_len(xs) : {B.Octets.split_at.pick(Nat.is_le(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys))), _, B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
460	      %Equal.sym(Nat, List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)), Nat.add(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys)), w8s_len_app(xs, ys)) : {B.Octets.split_at.pick(Nat.is_le(List.length(&2, B.OctByte, xs), _), List.length(&2, B.OctByte, xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
461	      %Equal.sym(Bool, Nat.is_le(List.length(&2, B.OctByte, xs), Nat.add(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys))), True{}, UO.nat_le_add_r(List.length(&2, B.OctByte, xs), List.length(&2, B.OctByte, ys))) : {B.Octets.split_at.pick(_, List.length(&2, B.OctByte, xs), B.Octets{List.append(&2, B.OctByte, xs, ys)}) == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
462	      %F_take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys)) : {Some{B.OctetsSplit{B.Octets{_}, B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}}} == Some{B.OctetsSplit{B.Octets{xs}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
463	      %w8s_take_app(xs, ys) : {Some{B.OctetsSplit{B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}, B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}}} == Some{B.OctetsSplit{B.Octets{_}, B.Octets{ys}}} : Maybe<&2, B.OctetsSplit>}
464	      %w8s_drop_app(xs, ys) : {Some{B.OctetsSplit{B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}, B.Octets{B.w8s.drop(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}}} == Some{B.OctetsSplit{B.Octets{B.w8s.take(List.length(&2, B.OctByte, xs), List.append(&2, B.OctByte, xs, ys))}, B.Octets{_}}} : Maybe<&2, B.OctetsSplit>}
465	      {==}
466	
467	def Laws.octets_split_at_append(a, b):
468	  p_octets_split_at_append(a, b)
469	
470	def Laws.octets_split_short():
471	  {==}
472	
473	def Laws.octets_split_text():
474	  {==}
475	
476	def p_octets_zeros_list(+n: Nat) -> {B.Octets.to_list(B.Octets.zeros(n)) == B.zeros(n) : List<&2, U32>}:
477	  %F_to(B.w8s.zeros.fast(n)) : {_ == B.zeros(n) : List<&2, U32>}
478	  %F_zeros(n) : {B.w8s.to_list(_) == B.zeros(n) : List<&2, U32>}
479	  w8s_zeros_list(n)
480	
481	def Laws.octets_zeros_list(n):
482	  p_octets_zeros_list(n)
483	
484	def p_octets_cons_list(+b: U32, +o: B.Octets) -> {B.Octets.to_list(B.Octets.cons(b, o)) == Con{B.byte(b), B.Octets.to_list(o)} : List<&2, U32>}:
485	  match o:
486	    case B.Octets{+ws}:
487	      %F_to(Con{B.oct.of(b), ws}) : {_ == Con{B.byte(b), B.w8s.to_list.fast(ws)} : List<&2, U32>}
488	      %F_to(ws) : {Con{B.oct.to(B.oct.of(b)), B.w8s.to_list(ws)} == Con{B.byte(b), _} : List<&2, U32>}
489	      %oct_byte(b) : {Con{B.oct.to(B.oct.of(b)), B.w8s.to_list(ws)} == Con{_, B.w8s.to_list(ws)} : List<&2, U32>}
490	      {==}
491	
492	def Laws.octets_cons_list(b, o):
493	  p_octets_cons_list(b, o)
494	
495	# The tail-recursive list layer equals the structural one
496	
497	def ru_app_nil(+xs: List<&2, U32>) -> {List.append(&2, U32, xs, Nil{}) == xs : List<&2, U32>}:
498	  app_nilu(xs)
499	
500	def g_lenu(+xs: List<&2, U32>, +n: Nat) -> {B.len.go(xs, n) == Nat.add(B.len(xs), n) : Nat}:
501	  match xs:
502	    case Nil{}:
503	      {==}
504	    case Con{h, t}:
505	      Equal.trans(Nat, B.len.go(t, 1n+n), Nat.add(B.len(t), 1n+n), 1n+Nat.add(B.len(t), n),
506	        g_lenu(t, 1n+n), UL.nat_add_succ(B.len(t), n))
507	
508	def p_len_fast(+xs: List<&2, U32>) -> {B.len(xs) == B.len.fast(xs) : Nat}:
509	  Equal.sym(Nat, B.len.fast(xs), B.len(xs),
510	    Equal.trans(Nat, B.len.go(xs, 0n), Nat.add(B.len(xs), 0n), B.len(xs), g_lenu(xs, 0n), UL.nat_add_zero(B.len(xs))))
511	
512	def Laws.len_fast(xs):
513	  p_len_fast(xs)
514	
515	# a structural list, reversed onto Nil and back, is itself
516	def rr_back(+zs: List<&2, U32>) -> {B.rev_onto(B.rev_onto(zs, Nil{}), Nil{}) == zs : List<&2, U32>}:
517	  Equal.trans(List<&2, U32>, B.rev_onto(B.rev_onto(zs, Nil{}), Nil{}), List.append(&2, U32, zs, Nil{}), zs, ru_rr(zs, Nil{}, Nil{}), app_nilu(zs))
518	
519	def g_takeu(+n: Nat, +xs: List<&2, U32>, +acc: List<&2, U32>) -> {B.take.go(n, xs, acc) == B.rev_onto(B.take(n, xs), acc) : List<&2, U32>}:
520	  match n xs:
521	    case 0n _:
522	      {==}
523	    case 1n+p Nil{}:
524	      {==}
525	    case 1n+p Con{h, t}:
526	      g_takeu(p, t, Con{h, acc})
527	
528	def p_take_fast(+n: Nat, +xs: List<&2, U32>) -> {B.take(n, xs) == B.take.fast(n, xs) : List<&2, U32>}:
529	  Equal.sym(List<&2, U32>, B.take.fast(n, xs), B.take(n, xs),
530	    Equal.trans(List<&2, U32>, B.take.fast(n, xs), B.rev_onto(B.rev_onto(B.take(n, xs), Nil{}), Nil{}), B.take(n, xs),
531	      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.take.go(n, xs, Nil{}), B.rev_onto(B.take(n, xs), Nil{}), g_takeu(n, xs, Nil{})),
532	      rr_back(B.take(n, xs))))
533	
534	def Laws.take_fast(n, xs):
535	  p_take_fast(n, xs)
536	
537	def p_append_fast(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {B.append(xs, ys) == B.append.fast(xs, ys) : List<&2, U32>}:
538	  Equal.sym(List<&2, U32>, B.append.fast(xs, ys), B.append(xs, ys), ru_rr(xs, Nil{}, ys))
539	
540	def Laws.append_fast(xs, ys):
541	  p_append_fast(xs, ys)
542	
543	def zeros_consu(+p: Nat, +acc: List<&2, U32>) -> {List.append(&2, U32, B.zeros(p), Con{0, acc}) == Con{0, List.append(&2, U32, B.zeros(p), acc)} : List<&2, U32>}:
544	  match p:
545	    case 0n:
546	      {==}
547	    case 1n+q:
548	      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{0, l}, List.append(&2, U32, B.zeros(q), Con{0, acc}), Con{0, List.append(&2, U32, B.zeros(q), acc)}, zeros_consu(q, acc))
549	
550	def g_zerosu(+n: Nat, +acc: List<&2, U32>) -> {B.zeros.go(n, acc) == List.append(&2, U32, B.zeros(n), acc) : List<&2, U32>}:
551	  match n:
552	    case 0n:
553	      {==}
554	    case 1n+p:
555	      Equal.trans(List<&2, U32>, B.zeros.go(p, Con{0, acc}), List.append(&2, U32, B.zeros(p), Con{0, acc}), Con{0, List.append(&2, U32, B.zeros(p), acc)},
556	        g_zerosu(p, Con{0, acc}), zeros_consu(p, acc))
557	
558	def p_zeros_fast(+n: Nat) -> {B.zeros(n) == B.zeros.fast(n) : List<&2, U32>}:
559	  Equal.sym(List<&2, U32>, B.zeros.fast(n), B.zeros(n),
560	    Equal.trans(List<&2, U32>, B.zeros.go(n, Nil{}), List.append(&2, U32, B.zeros(n), Nil{}), B.zeros(n), g_zerosu(n, Nil{}), app_nilu(B.zeros(n))))
561	
562	def Laws.zeros_fast(n):
563	  p_zeros_fast(n)
564	
565	def g_mask(+xs: List<&2, U32>, +acc: List<&2, U32>) -> {B.mask.go(xs, acc) == B.rev_onto(B.mask(xs), acc) : List<&2, U32>}:
566	  match xs:
567	    case Nil{}:
568	      {==}
569	    case Con{h, t}:
570	      g_mask(t, Con{B.byte(h), acc})
571	
572	def p_mask_fast(+xs: List<&2, U32>) -> {B.mask(xs) == B.mask.fast(xs) : List<&2, U32>}:
573	  Equal.sym(List<&2, U32>, B.mask.fast(xs), B.mask(xs),
574	    Equal.trans(List<&2, U32>, B.mask.fast(xs), B.rev_onto(B.rev_onto(B.mask(xs), Nil{}), Nil{}), B.mask(xs),
575	      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.mask.go(xs, Nil{}), B.rev_onto(B.mask(xs), Nil{}), g_mask(xs, Nil{})),
576	      rr_back(B.mask(xs))))
577	
578	def Laws.mask_fast(xs):
579	  p_mask_fast(xs)
580	
581	def g_of_string(+s: String, +acc: List<&2, U32>) -> {B.of_string.go(s, acc) == B.rev_onto(B.of_string(s), acc) : List<&2, U32>}:
582	  match s:
583	    case SNil{}:
584	      {==}
585	    case SCon{Chr{c}, t}:
586	      g_of_string(t, Con{B.byte(c), acc})
587	
588	def p_of_string_fast(+s: String) -> {B.of_string(s) == B.of_string.fast(s) : List<&2, U32>}:
589	  Equal.sym(List<&2, U32>, B.of_string.fast(s), B.of_string(s),
590	    Equal.trans(List<&2, U32>, B.of_string.fast(s), B.rev_onto(B.rev_onto(B.of_string(s), Nil{}), Nil{}), B.of_string(s),
591	      Equal.cong(List<&2, U32>, List<&2, U32>, l => B.rev_onto(l, Nil{}), B.of_string.go(s, Nil{}), B.rev_onto(B.of_string(s), Nil{}), g_of_string(s, Nil{})),
592	      rr_back(B.of_string(s))))
593	
594	def Laws.of_string_fast(s):
595	  p_of_string_fast(s)
596	
597	# text: building from the back onto acc is the structural cat
598	def t_go(+xs: List<&2, U32>, +r: List<&2, U32>, +acc: String) -> {B.to_string.go(B.rev_onto(xs, r), acc) == B.to_string.go(r, B.to_string.cat(xs, acc)) : String}:
599	  match xs:
600	    case Nil{}:
601	      {==}
602	    case Con{h, t}:
603	      t_go(t, Con{h, r}, acc)
604	
605	def t_cat(+xs: List<&2, U32>) -> {B.to_string.cat(xs, SNil{}) == B.to_string(xs) : String}:
606	  match xs:
607	    case Nil{}:
608	      {==}
609	    case Con{h, t}:
610	      Equal.cong(String, String, x => SCon{Chr{B.byte(h)}, x}, B.to_string.cat(t, SNil{}), B.to_string(t), t_cat(t))
611	
612	def p_to_string_fast(+xs: List<&2, U32>) -> {B.to_string(xs) == B.to_string.fast(xs) : String}:
613	  Equal.sym(String, B.to_string.fast(xs), B.to_string(xs),
614	    Equal.trans(String, B.to_string.go(B.rev_onto(xs, Nil{}), SNil{}), B.to_string.cat(xs, SNil{}), B.to_string(xs), t_go(xs, Nil{}, SNil{}), t_cat(xs)))
615	
616	def Laws.to_string_fast(xs):
617	  p_to_string_fast(xs)
618	
619	def h_go(+xs: List<&2, U32>, +r: List<&2, U32>, +acc: String) -> {B.hex.go(B.rev_onto(xs, r), acc) == B.hex.go(r, B.hex.cat(xs, acc)) : String}:
620	  match xs:
621	    case Nil{}:
622	      {==}
623	    case Con{h, t}:
624	      h_go(t, Con{h, r}, acc)
625	
626	def h_cat(+xs: List<&2, U32>) -> {B.hex.cat(xs, SNil{}) == B.hex(xs) : String}:
627	  match xs:
628	    case Nil{}:
629	      {==}
630	    case Con{h, t}:
631	      Equal.cong(String, String, x => SCon{B.hex.digit(U32.shrn(B.byte(h), 4n)), SCon{B.hex.digit(U32.and(B.byte(h), 15)), x}}, B.hex.cat(t, SNil{}), B.hex(t), h_cat(t))
632	
633	def p_hex_fast(+xs: List<&2, U32>) -> {B.hex(xs) == B.hex.fast(xs) : String}:
634	  Equal.sym(String, B.hex.fast(xs), B.hex(xs),
635	    Equal.trans(String, B.hex.go(B.rev_onto(xs, Nil{}), SNil{}), B.hex.cat(xs, SNil{}), B.hex(xs), h_go(xs, Nil{}, SNil{}), h_cat(xs)))
636	
637	def Laws.hex_fast(xs):
638	  p_hex_fast(xs)
639	
640	def eq_go(+xs: List<&2, U32>, +ys: List<&2, U32>, +ok: Bool) -> {B.list_eq.go(xs, ys, ok) == Bool.and(ok, B.list_eq(xs, ys)) : Bool}:
641	  match xs ys:
642	    case Nil{} Nil{}:
643	      match ok:
644	        case True{}:
645	          {==}
646	        case False{}:
647	          {==}
648	    case Con{a, s} Con{b, t}:
649	      match ok:
650	        case True{}:
651	          eq_go(s, t, U32.is_eq(a, b))
652	        case False{}:
653	          eq_go(s, t, False{})
654	    case Nil{} Con{b, t}:
655	      match ok:
656	        case True{}:
657	          {==}
658	        case False{}:
659	          {==}
660	    case Con{a, s} Nil{}:
661	      match ok:
662	        case True{}:
663	          {==}
664	        case False{}:
665	          {==}
666	
667	def p_list_eq_fast(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {B.list_eq(xs, ys) == B.list_eq.fast(xs, ys) : Bool}:
668	  Equal.sym(Bool, B.list_eq.fast(xs, ys), B.list_eq(xs, ys), eq_go(xs, ys, True{}))
669	
670	def Laws.list_eq_fast(xs, ys):
671	  p_list_eq_fast(xs, ys)
672	
673	def Laws.rev_rev(xs):
674	  rr_back(xs)
675	
676	# Octets' text and hex: each word read through bits8/of_bits8 is its byte
677	def w_t_go(+ws: List<&2, B.OctByte>, +r: List<&2, B.OctByte>, +acc: String) -> {B.w8s.text.go(B.w8s.rev_onto(ws, r), acc) == B.w8s.text.go(r, B.to_string.cat(B.w8s.to_list(ws), acc)) : String}:
678	  match ws:
679	    case Nil{}:
680	      {==}
681	    case Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, t}:
682	      w_t_go(t, Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, r}, acc)
683	
684	def p_octets_to_string_list(+o: B.Octets) -> {B.Octets.to_string(o) == B.to_string(B.Octets.to_list(o)) : String}:
685	  match o:
686	    case B.Octets{+ws}:
687	      %F_to(ws) : {B.w8s.text.go(B.w8s.rev_onto(ws, Nil{}), SNil{}) == B.to_string(_) : String}
688	      Equal.trans(String, B.w8s.text.go(B.w8s.rev_onto(ws, Nil{}), SNil{}), B.to_string.cat(B.w8s.to_list(ws), SNil{}), B.to_string(B.w8s.to_list(ws)), w_t_go(ws, Nil{}, SNil{}), t_cat(B.w8s.to_list(ws)))
689	
690	def Laws.octets_to_string_list(o):
691	  p_octets_to_string_list(o)
692	
693	def w_h_go(+ws: List<&2, B.OctByte>, +r: List<&2, B.OctByte>, +acc: String) -> {B.w8s.hex.go(B.w8s.rev_onto(ws, r), acc) == B.w8s.hex.go(r, B.hex.cat(B.w8s.to_list(ws), acc)) : String}:
694	  match ws:
695	    case Nil{}:
696	      {==}
697	    case Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, t}:
698	      w_h_go(t, Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, r}, acc)
699	
700	def p_octets_hex_list(+o: B.Octets) -> {B.Octets.hex(o) == B.hex(B.Octets.to_list(o)) : String}:
701	  match o:
702	    case B.Octets{+ws}:
703	      %F_to(ws) : {B.w8s.hex.go(B.w8s.rev_onto(ws, Nil{}), SNil{}) == B.hex(_) : String}
704	      Equal.trans(String, B.w8s.hex.go(B.w8s.rev_onto(ws, Nil{}), SNil{}), B.hex.cat(B.w8s.to_list(ws), SNil{}), B.hex(B.w8s.to_list(ws)), w_h_go(ws, Nil{}, SNil{}), h_cat(B.w8s.to_list(ws)))
705	
706	def Laws.octets_hex_list(o):
707	  p_octets_hex_list(o)
708	
709	# concat: pushing each piece's words is reversing the joined words
710	def rev_app8(+xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, +acc: List<&2, B.OctByte>) -> {B.w8s.rev_onto(List.append(&2, B.OctByte, xs, ys), acc) == B.w8s.rev_onto(ys, B.w8s.rev_onto(xs, acc)) : List<&2, B.OctByte>}:
711	  match xs:
712	    case Nil{}:
713	      {==}
714	    case Con{h, t}:
715	      rev_app8(t, ys, Con{h, acc})
716	
717	def concat_step(+ws: List<&2, B.OctByte>, +c: B.Octets, +acc: List<&2, B.OctByte>) -> {B.w8s.rev_onto(B.Octets.words(c), B.w8s.rev_onto(ws, acc)) == B.w8s.rev_onto(B.Octets.words(B.Octets.append(B.Octets{ws}, c)), acc) : List<&2, B.OctByte>}:
718	  match c:
719	    case B.Octets{+zs}:
720	      %F_app(ws, zs) : {B.w8s.rev_onto(zs, B.w8s.rev_onto(ws, acc)) == B.w8s.rev_onto(_, acc) : List<&2, B.OctByte>}
721	      Equal.sym(List<&2, B.OctByte>, B.w8s.rev_onto(List.append(&2, B.OctByte, ws, zs), acc), B.w8s.rev_onto(zs, B.w8s.rev_onto(ws, acc)), rev_app8(ws, zs, acc))
722	
723	def concat_go(+os: List<&2, B.Octets>, +acc: List<&2, B.OctByte>) -> {B.w8s.concat.go(os, acc) == B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(os)), acc) : List<&2, B.OctByte>}:
724	  match os:
725	    case Nil{}:
726	      {==}
727	    case Con{B.Octets{+ws}, t}:
728	      Equal.trans(List<&2, B.OctByte>, B.w8s.concat.go(t, B.w8s.rev_onto(ws, acc)), B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(t)), B.w8s.rev_onto(ws, acc)), B.w8s.rev_onto(B.Octets.words(B.Octets.append(B.Octets{ws}, B.Octets.concat.ref(t))), acc),
729	        concat_go(t, B.w8s.rev_onto(ws, acc)), concat_step(ws, B.Octets.concat.ref(t), acc))
730	
731	def octets_eta(+o: B.Octets) -> {B.Octets{B.Octets.words(o)} == o : B.Octets}:
732	  match o:
733	    case B.Octets{ws}:
734	      {==}
735	
736	def rr8_back(+zs: List<&2, B.OctByte>) -> {B.w8s.rev_onto(B.w8s.rev_onto(zs, Nil{}), Nil{}) == zs : List<&2, B.OctByte>}:
737	  Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.rev_onto(zs, Nil{}), Nil{}), List.append(&2, B.OctByte, zs, Nil{}), zs, r8_rr(zs, Nil{}, Nil{}), app_nil8(zs))
738	
739	def concat_ref(+os: List<&2, B.Octets>) -> {B.Octets.concat(os) == B.Octets.concat.ref(os) : B.Octets}:
740	  Equal.trans(B.Octets, B.Octets.concat(os), B.Octets{B.Octets.words(B.Octets.concat.ref(os))}, B.Octets.concat.ref(os),
741	    Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.rev_onto(B.w8s.concat.go(os, Nil{}), Nil{}), B.Octets.words(B.Octets.concat.ref(os)),
742	      Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.concat.go(os, Nil{}), Nil{}), B.w8s.rev_onto(B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(os)), Nil{}), Nil{}), B.Octets.words(B.Octets.concat.ref(os)),
743	        Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => B.w8s.rev_onto(l, Nil{}), B.w8s.concat.go(os, Nil{}), B.w8s.rev_onto(B.Octets.words(B.Octets.concat.ref(os)), Nil{}), concat_go(os, Nil{})),
744	        rr8_back(B.Octets.words(B.Octets.concat.ref(os))))),
745	    octets_eta(B.Octets.concat.ref(os)))
746	
747	def Laws.octets_concat_nil():
748	  {==}
749	
750	def p_octets_concat_cons(+h: B.Octets, +t: List<&2, B.Octets>) -> {B.Octets.concat(Con{h, t}) == B.Octets.append(h, B.Octets.concat(t)) : B.Octets}:
751	  %Equal.sym(B.Octets, B.Octets.concat(t), B.Octets.concat.ref(t), concat_ref(t)) : {B.Octets.concat(Con{h, t}) == B.Octets.append(h, _) : B.Octets}
752	  concat_ref(Con{h, t})
753	
754	def Laws.octets_concat_cons(h, t):
755	  p_octets_concat_cons(h, t)
756	
757	# Reading at offsets: lemmas
758	
759	def off.disc(b: Bool) -> Type:
760	  match b:
761	    case True{}:
762	      Unit
763	    case False{}:
764	      Empty
765	
766	def off.clash(h: {False{} == True{} : Bool}) -> Empty:
767	  %Equal.sym(Bool, False{}, True{}, h) : off.disc(_)
768	  Unit{}
769	
770	def off.absurd(-A: Type, e: Empty) -> A:
771	  match e:
772	
773	def off.no(-A: Type, h: {False{} == True{} : Bool}) -> A:
774	  off.absurd(A, off.clash(h))
775	
776	# Natural numbers
777	
778	def off.le_zero(+m: Nat) -> {Nat.is_le(0n, m) == True{} : Bool}:
779	  match m:
780	    case 0n:
781	      {==}
782	    case 1n+p:
783	      {==}
784	
785	# i + n <= m: i <= m
786	def off.le_add_l(+i: Nat, +n: Nat, +m: Nat) -> {Nat.is_le(Nat.add(i, n), m) == True{} : Bool} -> {Nat.is_le(i, m) == True{} : Bool}:
787	  match i m:
788	    case 0n _:
789	      h => off.le_zero(m)
790	    case 1n+p 0n:
791	      h => off.no({Nat.is_le(1n+p, 0n) == True{} : Bool}, h)
792	    case 1n+p 1n+q:
793	      h => off.le_add_l(p, n, q, h)
794	
795	# i + n <= m: n <= m - i
796	def off.le_sub(+i: Nat, +n: Nat, +m: Nat) -> {Nat.is_le(Nat.add(i, n), m) == True{} : Bool} -> {Nat.is_le(n, Nat.sub(m, i)) == True{} : Bool}:
797	  match i m:
798	    case 0n 0n:
799	      h => h
800	    case 0n 1n+q:
801	      h => h
802	    case 1n+p 0n:
803	      h => off.no({Nat.is_le(n, Nat.sub(0n, 1n+p)) == True{} : Bool}, h)
804	    case 1n+p 1n+q:
805	      h => off.le_sub(p, n, q, h)
806	
807	# n <= k: min(n, k) == n
808	def off.min_le(+n: Nat, +k: Nat) -> {Nat.is_le(n, k) == True{} : Bool} -> {Nat.min(n, k) == n : Nat}:
809	  match n k:
810	    case 0n _:
811	      h => {==}
812	    case 1n+p 0n:
813	      h => off.no({Nat.min(1n+p, 0n) == 1n+p : Nat}, h)
814	    case 1n+p 1n+q:
815	      h => Equal.cong(Nat, Nat, x => 1n+x, Nat.min(p, q), p, off.min_le(p, q, h))
816	
817	# Word lists
818	
819	def off.drop_nil(+i: Nat) -> {B.w8s.drop(i, Nil{}) == Nil{} : List<&2, B.OctByte>}:
820	  match i:
821	    case 0n:
822	      {==}
823	    case 1n+p:
824	      {==}
825	
826	def off.take_nil(+i: Nat) -> {B.w8s.take(i, Nil{}) == Nil{} : List<&2, B.OctByte>}:
827	  match i:
828	    case 0n:
829	      {==}
830	    case 1n+p:
831	      {==}
832	
833	def off.drop_app_add(xs: List<&2, B.OctByte>, +n: Nat, +ys: List<&2, B.OctByte>) -> {B.w8s.drop(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)) == B.w8s.drop(n, ys) : List<&2, B.OctByte>}:
834	  match xs:
835	    case Nil{}:
836	      {==}
837	    case Con{h, t}:
838	      off.drop_app_add(t, n, ys)
839	
840	def off.take_app_add(xs: List<&2, B.OctByte>, +n: Nat, +ys: List<&2, B.OctByte>) -> {B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)) == List.append(&2, B.OctByte, xs, B.w8s.take(n, ys)) : List<&2, B.OctByte>}:
841	  match xs:
842	    case Nil{}:
843	      {==}
844	    case Con{h, t}:
845	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, B.w8s.take(Nat.add(List.length(&2, B.OctByte, t), n), List.append(&2, B.OctByte, t, ys)), List.append(&2, B.OctByte, t, B.w8s.take(n, ys)), off.take_app_add(t, n, ys))
846	
847	def off.take_app_le(+n: Nat, xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool} -> {B.w8s.take(n, List.append(&2, B.OctByte, xs, ys)) == B.w8s.take(n, xs) : List<&2, B.OctByte>}:
848	  match n xs:
849	    case 0n _:
850	      h => {==}
851	    case 1n+p Nil{}:
852	      h => off.no({B.w8s.take(1n+p, ys) == Nil{} : List<&2, B.OctByte>}, h)
853	    case 1n+p Con{x, t}:
854	      h => Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{x, l}, B.w8s.take(p, List.append(&2, B.OctByte, t, ys)), B.w8s.take(p, t), off.take_app_le(p, t, ys, h))
855	
856	def off.drop_app_le(+n: Nat, xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool} -> {B.w8s.drop(n, List.append(&2, B.OctByte, xs, ys)) == List.append(&2, B.OctByte, B.w8s.drop(n, xs), ys) : List<&2, B.OctByte>}:
857	  match n xs:
858	    case 0n _:
859	      h => {==}
860	    case 1n+p Nil{}:
861	      h => off.no({B.w8s.drop(1n+p, ys) == ys : List<&2, B.OctByte>}, h)
862	    case 1n+p Con{x, t}:
863	      h => off.drop_app_le(p, t, ys, h)
864	
865	def off.drop_drop(+j: Nat, +i: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.drop(i, B.w8s.drop(j, ws)) == B.w8s.drop(Nat.add(j, i), ws) : List<&2, B.OctByte>}:
866	  match j ws:
867	    case 0n _:
868	      {==}
869	    case 1n+q Nil{}:
870	      off.drop_nil(i)
871	    case 1n+q Con{x, t}:
872	      off.drop_drop(q, i, t)
873	
874	def off.take_take(+i: Nat, +j: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.take(i, B.w8s.take(j, ws)) == B.w8s.take(Nat.min(i, j), ws) : List<&2, B.OctByte>}:
875	  match i j ws:
876	    case 0n _ _:
877	      {==}
878	    case 1n+p 0n _:
879	      {==}
880	    case 1n+p 1n+q Nil{}:
881	      {==}
882	    case 1n+p 1n+q Con{x, t}:
883	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{x, l}, B.w8s.take(p, B.w8s.take(q, t)), B.w8s.take(Nat.min(p, q), t), off.take_take(p, q, t))
884	
885	def off.take_drop(+i: Nat, +j: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.take(i, B.w8s.drop(j, ws)) == B.w8s.drop(j, B.w8s.take(Nat.add(j, i), ws)) : List<&2, B.OctByte>}:
886	  match j ws:
887	    case 0n _:
888	      {==}
889	    case 1n+q Nil{}:
890	      off.take_nil(i)
891	    case 1n+q Con{x, t}:
892	      off.take_drop(i, q, t)
893	
894	def off.drop_take(+i: Nat, +j: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.drop(i, B.w8s.take(j, ws)) == B.w8s.take(Nat.sub(j, i), B.w8s.drop(i, ws)) : List<&2, B.OctByte>}:
895	  match i j ws:
896	    case 0n 0n _:
897	      {==}
898	    case 0n 1n+q _:
899	      {==}
900	    case 1n+p 0n _:
901	      {==}
902	    case 1n+p 1n+q Nil{}:
903	      Equal.sym(List<&2, B.OctByte>, B.w8s.take(Nat.sub(q, p), Nil{}), Nil{}, off.take_nil(Nat.sub(q, p)))
904	    case 1n+p 1n+q Con{x, t}:
905	      off.drop_take(p, q, t)
906	
907	def off.len_take(+n: Nat, ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, B.w8s.take(n, ws)) == Nat.min(n, List.length(&2, B.OctByte, ws)) : Nat}:
908	  match n ws:
909	    case 0n _:
910	      {==}
911	    case 1n+p Nil{}:
912	      {==}
913	    case 1n+p Con{x, t}:
914	      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, B.w8s.take(p, t)), Nat.min(p, List.length(&2, B.OctByte, t)), off.len_take(p, t))
915	
916	def off.len_drop(+n: Nat, ws: List<&2, B.OctByte>) -> {List.length(&2, B.OctByte, B.w8s.drop(n, ws)) == Nat.sub(List.length(&2, B.OctByte, ws), n) : Nat}:
917	  match n ws:
918	    case 0n Nil{}:
919	      {==}
920	    case 0n Con{x, t}:
921	      {==}
922	    case 1n+p Nil{}:
923	      {==}
924	    case 1n+p Con{x, t}:
925	      off.len_drop(p, t)
926	
927	def off.len_zeros(+n: Nat) -> {List.length(&2, B.OctByte, B.w8s.zeros(n)) == n : Nat}:
928	  match n:
929	    case 0n:
930	      {==}
931	    case 1n+p:
932	      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, B.w8s.zeros(p)), p, off.len_zeros(p))
933	
934	def off.len_of(xs: List<&2, U32>) -> {List.length(&2, B.OctByte, B.w8s.of_list(xs)) == B.len(xs) : Nat}:
935	  match xs:
936	    case Nil{}:
937	      {==}
938	    case Con{h, t}:
939	      Equal.cong(Nat, Nat, k => 1n+k, List.length(&2, B.OctByte, B.w8s.of_list(t)), B.len(t), off.len_of(t))
940	
941	def off.app_assoc(xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, +zs: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys), zs) == List.append(&2, B.OctByte, xs, List.append(&2, B.OctByte, ys, zs)) : List<&2, B.OctByte>}:
942	  match xs:
943	    case Nil{}:
944	      {==}
945	    case Con{h, t}:
946	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, List.append(&2, B.OctByte, List.append(&2, B.OctByte, t, ys), zs), List.append(&2, B.OctByte, t, List.append(&2, B.OctByte, ys, zs)), off.app_assoc(t, ys, zs))
947	
948	# a byte: at the head of what is left after the offset
949	
950	def off.at_app_lt(+i: Nat, xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>) -> {Nat.is_lt(i, List.length(&2, B.OctByte, xs)) == True{} : Bool} -> {B.w8s.at(B.w8s.drop(i, List.append(&2, B.OctByte, xs, ys))) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}:
951	  match i xs:
952	    case 0n Nil{}:
953	      h => off.no({B.w8s.at(ys) == None{} : Maybe<&2, U32>}, h)
954	    case 1n+p Nil{}:
955	      h => off.no({B.w8s.at(B.w8s.drop(1n+p, ys)) == None{} : Maybe<&2, U32>}, h)
956	    case 0n Con{x, t}:
957	      h => {==}
958	    case 1n+p Con{x, t}:
959	      h => off.at_app_lt(p, t, ys, h)
960	
961	def off.at_take(+i: Nat, +n: Nat, ws: List<&2, B.OctByte>) -> {Nat.is_lt(i, n) == True{} : Bool} -> {B.w8s.at(B.w8s.drop(i, B.w8s.take(n, ws))) == B.w8s.at(B.w8s.drop(i, ws)) : Maybe<&2, U32>}:
962	  match i n ws:
963	    case 0n 0n _:
964	      h => off.no({B.w8s.at(Nil{}) == B.w8s.at(ws) : Maybe<&2, U32>}, h)
965	    case 1n+p 0n _:
966	      h => off.no({B.w8s.at(B.w8s.drop(1n+p, Nil{})) == B.w8s.at(B.w8s.drop(1n+p, ws)) : Maybe<&2, U32>}, h)
967	    case 0n 1n+q Nil{}:
968	      h => {==}
969	    case 0n 1n+q Con{x, t}:
970	      h => {==}
971	    case 1n+p 1n+q Nil{}:
972	      h => {==}
973	    case 1n+p 1n+q Con{x, t}:
974	      h => off.at_take(p, q, t, h)
975	
976	def off.at_to(+i: Nat, ws: List<&2, B.OctByte>) -> {B.w8s.at(B.w8s.drop(i, ws)) == B.at(B.w8s.to_list(ws), i) : Maybe<&2, U32>}:
977	  match i ws:
978	    case 0n Nil{}:
979	      {==}
980	    case 1n+p Nil{}:
981	      {==}
982	    case 0n Con{B.OctByte{a0, a1, a2, a3, a4, a5, a6, a7}, t}:
983	      {==}
984	    case 1n+p Con{x, t}:
985	      off.at_to(p, t)
986	
987	# The list layer
988	
989	def off.ldrop_app_add(a: List<&2, U32>, +n: Nat, +b: List<&2, U32>) -> {B.drop(Nat.add(B.len(a), n), B.append(a, b)) == B.drop(n, b) : List<&2, U32>}:
990	  match a:
991	    case Nil{}:
992	      {==}
993	    case Con{h, t}:
994	      off.ldrop_app_add(t, n, b)
995	
996	def off.lat_app_lt(+i: Nat, a: List<&2, U32>, +b: List<&2, U32>) -> {Nat.is_lt(i, B.len(a)) == True{} : Bool} -> {B.at(B.append(a, b), i) == B.at(a, i) : Maybe<&2, U32>}:
997	  match i a:
998	    case 0n Nil{}:
999	      h => off.no({B.at(b, 0n) == None{} : Maybe<&2, U32>}, h)
1000	    case 1n+p Nil{}:
1001	      h => off.no({B.at(b, 1n+p) == B.at(Nil{}, 1n+p) : Maybe<&2, U32>}, h)
1002	    case 0n Con{x, t}:
1003	      h => {==}
1004	    case 1n+p Con{x, t}:
1005	      h => off.lat_app_lt(p, t, b, h)
1006	
1007	def off.ldrop_nil(+i: Nat) -> {B.drop(i, Nil{}) == Nil{} : List<&2, U32>}:
1008	  match i:
1009	    case 0n:
1010	      {==}
1011	    case 1n+p:
1012	      {==}
1013	
1014	def off.ldrop_drop(+j: Nat, +i: Nat, xs: List<&2, U32>) -> {B.drop(i, B.drop(j, xs)) == B.drop(Nat.add(j, i), xs) : List<&2, U32>}:
1015	  match j xs:
1016	    case 0n _:
1017	      {==}
1018	    case 1n+q Nil{}:
1019	      off.ldrop_nil(i)
1020	    case 1n+q Con{x, t}:
1021	      off.ldrop_drop(q, i, t)
1022	
1023	def off.lat_take(+i: Nat, +n: Nat, xs: List<&2, U32>) -> {Nat.is_lt(i, n) == True{} : Bool} -> {B.at(B.take(n, xs), i) == B.at(xs, i) : Maybe<&2, U32>}:
1024	  match i n xs:
1025	    case 0n 0n _:
1026	      h => off.no({B.at(Nil{}, 0n) == B.at(xs, 0n) : Maybe<&2, U32>}, h)
1027	    case 1n+p 0n _:
1028	      h => off.no({B.at(Nil{}, 1n+p) == B.at(xs, 1n+p) : Maybe<&2, U32>}, h)
1029	    case 0n 1n+q Nil{}:
1030	      h => {==}
1031	    case 0n 1n+q Con{x, t}:
1032	      h => {==}
1033	    case 1n+p 1n+q Nil{}:
1034	      h => {==}
1035	    case 1n+p 1n+q Con{x, t}:
1036	      h => off.lat_take(p, q, t, h)
1037	
1038	def off.llen_app(a: List<&2, U32>, +b: List<&2, U32>) -> {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}:
1039	  match a:
1040	    case Nil{}:
1041	      {==}
1042	    case Con{h, t}:
1043	      Equal.cong(Nat, Nat, k => 1n+k, B.len(B.append(t, b)), Nat.add(B.len(t), B.len(b)), off.llen_app(t, b))
1044	
1045	def off.llen_le32(+v: U32) -> {B.len(B.le32(v)) == 4n : Nat}:
1046	  match v:
1047	    case U32{w}:
1048	      {==}
1049	
1050	def off.llen_be32(+v: U32) -> {B.len(B.be32(v)) == 4n : Nat}:
1051	  match v:
1052	    case U32{w}:
1053	      {==}
1054	
1055	def off.llen_le16(+v: U32) -> {B.len(B.le16(v)) == 2n : Nat}:
1056	  match v:
1057	    case U32{w}:
1058	      {==}
1059	
1060	def off.llen_be16(+v: U32) -> {B.len(B.be16(v)) == 2n : Nat}:
1061	  match v:
1062	    case U32{w}:
1063	      {==}
1064	
1065	def off.add_le32(+x: U32, +y: U32) -> {Nat.add(B.len(B.le32(x)), B.len(B.le32(y))) == 8n : Nat}:
1066	  match x y:
1067	    case U32{a} U32{b}:
1068	      {==}
1069	
1070	def off.add_be32(+x: U32, +y: U32) -> {Nat.add(B.len(B.be32(x)), B.len(B.be32(y))) == 8n : Nat}:
1071	  match x y:
1072	    case U32{a} U32{b}:
1073	      {==}
1074	
1075	def off.llen_le64(+v: W.W64) -> {B.len(B.le64(v)) == 8n : Nat}:
1076	  Equal.trans(Nat, B.len(B.le64(v)), Nat.add(B.len(B.le32(W.W64.lo(v))), B.len(B.le32(W.W64.hi(v)))), 8n, off.llen_app(B.le32(W.W64.lo(v)), B.le32(W.W64.hi(v))), off.add_le32(W.W64.lo(v), W.W64.hi(v)))
1077	
1078	def off.llen_be64(+v: W.W64) -> {B.len(B.be64(v)) == 8n : Nat}:
1079	  Equal.trans(Nat, B.len(B.be64(v)), Nat.add(B.len(B.be32(W.W64.hi(v))), B.len(B.be32(W.W64.lo(v)))), 8n, off.llen_app(B.be32(W.W64.hi(v)), B.be32(W.W64.lo(v))), off.add_be32(W.W64.hi(v), W.W64.lo(v)))
1080	
1081	# Octets: lengths
1082	
1083	def p_len_append(+a: B.Octets, +b: B.Octets) -> {B.Octets.len(B.Octets.append(a, b)) == Nat.add(B.Octets.len(a), B.Octets.len(b)) : Nat}:
1084	  match a b:
1085	    case B.Octets{+xs} B.Octets{+ys}:
1086	      %F_app(xs, ys) : {B.w8s.len.fast(_) == Nat.add(B.w8s.len.fast(xs), B.w8s.len.fast(ys)) : Nat}
1087	      %F_len(List.append(&2, B.OctByte, xs, ys)) : {_ == Nat.add(B.w8s.len.fast(xs), B.w8s.len.fast(ys)) : Nat}
1088	      %F_len(xs) : {List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)) == Nat.add(_, B.w8s.len.fast(ys)) : Nat}
1089	      %F_len(ys) : {List.length(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys)) == Nat.add(List.length(&2, B.OctByte, xs), _) : Nat}
1090	      w8s_len_app(xs, ys)
1091	
1092	def p_len_take(+n: Nat, +o: B.Octets) -> {B.Octets.len(B.Octets.take(n, o)) == Nat.min(n, B.Octets.len(o)) : Nat}:
1093	  match o:
1094	    case B.Octets{+ws}:
1095	      %F_take(n, ws) : {B.w8s.len.fast(_) == Nat.min(n, B.w8s.len.fast(ws)) : Nat}
1096	      %F_len(B.w8s.take(n, ws)) : {_ == Nat.min(n, B.w8s.len.fast(ws)) : Nat}
1097	      %F_len(ws) : {List.length(&2, B.OctByte, B.w8s.take(n, ws)) == Nat.min(n, _) : Nat}
1098	      off.len_take(n, ws)
1099	
1100	def p_len_drop(+n: Nat, +o: B.Octets) -> {B.Octets.len(B.Octets.drop(n, o)) == Nat.sub(B.Octets.len(o), n) : Nat}:
1101	  match o:
1102	    case B.Octets{+ws}:
1103	      %F_len(B.w8s.drop(n, ws)) : {_ == Nat.sub(B.w8s.len.fast(ws), n) : Nat}
1104	      %F_len(ws) : {List.length(&2, B.OctByte, B.w8s.drop(n, ws)) == Nat.sub(_, n) : Nat}
1105	      off.len_drop(n, ws)
1106	
1107	def p_len_take_le(+n: Nat, +o: B.Octets, h: {Nat.is_le(n, B.Octets.len(o)) == True{} : Bool}) -> {B.Octets.len(B.Octets.take(n, o)) == n : Nat}:
1108	  Equal.trans(Nat, B.Octets.len(B.Octets.take(n, o)), Nat.min(n, B.Octets.len(o)), n, p_len_take(n, o), off.min_le(n, B.Octets.len(o), h))
1109	
1110	def p_len_slice(+i: Nat, +n: Nat, +o: B.Octets) -> {B.Octets.len(B.Octets.slice(i, n, o)) == Nat.min(n, Nat.sub(B.Octets.len(o), i)) : Nat}:
1111	  Equal.trans(Nat, B.Octets.len(B.Octets.take(n, B.Octets.drop(i, o))), Nat.min(n, B.Octets.len(B.Octets.drop(i, o))), Nat.min(n, Nat.sub(B.Octets.len(o), i)),
1112	    p_len_take(n, B.Octets.drop(i, o)),
1113	    Equal.cong(Nat, Nat, k => Nat.min(n, k), B.Octets.len(B.Octets.drop(i, o)), Nat.sub(B.Octets.len(o), i), p_len_drop(i, o)))
1114	
1115	def p_len_slice_le(+i: Nat, +n: Nat, +o: B.Octets, h: {Nat.is_le(Nat.add(i, n), B.Octets.len(o)) == True{} : Bool}) -> {B.Octets.len(B.Octets.slice(i, n, o)) == n : Nat}:
1116	  Equal.trans(Nat, B.Octets.len(B.Octets.slice(i, n, o)), Nat.min(n, Nat.sub(B.Octets.len(o), i)), n, p_len_slice(i, n, o), off.min_le(n, Nat.sub(B.Octets.len(o), i), off.le_sub(i, n, B.Octets.len(o), h)))
1117	
1118	def p_len_zeros(+n: Nat) -> {B.Octets.len(B.Octets.zeros(n)) == n : Nat}:
1119	  %F_zeros(n) : {B.w8s.len.fast(_) == n : Nat}
1120	  %F_len(B.w8s.zeros(n)) : {_ == n : Nat}
1121	  off.len_zeros(n)
1122	
1123	def p_len_of_list(+xs: List<&2, U32>) -> {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat}:
1124	  %F_of(xs) : {B.w8s.len.fast(_) == B.len(xs) : Nat}
1125	  %F_len(B.w8s.of_list(xs)) : {_ == B.len(xs) : Nat}
1126	  off.len_of(xs)
1127	
1128	def p_append_assoc(+a: B.Octets, +b: B.Octets, +c: B.Octets) -> {B.Octets.append(B.Octets.append(a, b), c) == B.Octets.append(a, B.Octets.append(b, c)) : B.Octets}:
1129	  match a b c:
1130	    case B.Octets{+xs} B.Octets{+ys} B.Octets{+zs}:
1131	      %F_app(xs, ys) : {B.Octets{B.w8s.append.fast(_, zs)} == B.Octets{B.w8s.append.fast(xs, B.w8s.append.fast(ys, zs))} : B.Octets}
1132	      %F_app(ys, zs) : {B.Octets{B.w8s.append.fast(List.append(&2, B.OctByte, xs, ys), zs)} == B.Octets{B.w8s.append.fast(xs, _)} : B.Octets}
1133	      %F_app(List.append(&2, B.OctByte, xs, ys), zs) : {B.Octets{_} == B.Octets{B.w8s.append.fast(xs, List.append(&2, B.OctByte, ys, zs))} : B.Octets}
1134	      %F_app(xs, List.append(&2, B.OctByte, ys, zs)) : {B.Octets{List.append(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys), zs)} == B.Octets{_} : B.Octets}
1135	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, List.append(&2, B.OctByte, List.append(&2, B.OctByte, xs, ys), zs), List.append(&2, B.OctByte, xs, List.append(&2, B.OctByte, ys, zs)), off.app_assoc(xs, ys, zs))
1136	
1137	# Octets: take and drop composed
1138	
1139	def p_drop_drop(+j: Nat, +i: Nat, +o: B.Octets) -> {B.Octets.drop(i, B.Octets.drop(j, o)) == B.Octets.drop(Nat.add(j, i), o) : B.Octets}:
1140	  match o:
1141	    case B.Octets{+ws}:
1142	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(i, B.w8s.drop(j, ws)), B.w8s.drop(Nat.add(j, i), ws), off.drop_drop(j, i, ws))
1143	
1144	def p_take_take(+i: Nat, +j: Nat, +o: B.Octets) -> {B.Octets.take(i, B.Octets.take(j, o)) == B.Octets.take(Nat.min(i, j), o) : B.Octets}:
1145	  match o:
1146	    case B.Octets{+ws}:
1147	      %F_take(j, ws) : {B.Octets{B.w8s.take.fast(i, _)} == B.Octets{B.w8s.take.fast(Nat.min(i, j), ws)} : B.Octets}
1148	      %F_take(i, B.w8s.take(j, ws)) : {B.Octets{_} == B.Octets{B.w8s.take.fast(Nat.min(i, j), ws)} : B.Octets}
1149	      %F_take(Nat.min(i, j), ws) : {B.Octets{B.w8s.take(i, B.w8s.take(j, ws))} == B.Octets{_} : B.Octets}
1150	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(i, B.w8s.take(j, ws)), B.w8s.take(Nat.min(i, j), ws), off.take_take(i, j, ws))
1151	
1152	def p_take_drop(+i: Nat, +j: Nat, +o: B.Octets) -> {B.Octets.take(i, B.Octets.drop(j, o)) == B.Octets.drop(j, B.Octets.take(Nat.add(j, i), o)) : B.Octets}:
1153	  match o:
1154	    case B.Octets{+ws}:
1155	      %F_take(i, B.w8s.drop(j, ws)) : {B.Octets{_} == B.Octets{B.w8s.drop(j, B.w8s.take.fast(Nat.add(j, i), ws))} : B.Octets}
1156	      %F_take(Nat.add(j, i), ws) : {B.Octets{B.w8s.take(i, B.w8s.drop(j, ws))} == B.Octets{B.w8s.drop(j, _)} : B.Octets}
1157	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(i, B.w8s.drop(j, ws)), B.w8s.drop(j, B.w8s.take(Nat.add(j, i), ws)), off.take_drop(i, j, ws))
1158	
1159	def p_drop_take(+i: Nat, +j: Nat, +o: B.Octets) -> {B.Octets.drop(i, B.Octets.take(j, o)) == B.Octets.take(Nat.sub(j, i), B.Octets.drop(i, o)) : B.Octets}:
1160	  match o:
1161	    case B.Octets{+ws}:
1162	      %F_take(j, ws) : {B.Octets{B.w8s.drop(i, _)} == B.Octets{B.w8s.take.fast(Nat.sub(j, i), B.w8s.drop(i, ws))} : B.Octets}
1163	      %F_take(Nat.sub(j, i), B.w8s.drop(i, ws)) : {B.Octets{B.w8s.drop(i, B.w8s.take(j, ws))} == B.Octets{_} : B.Octets}
1164	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(i, B.w8s.take(j, ws)), B.w8s.take(Nat.sub(j, i), B.w8s.drop(i, ws)), off.drop_take(i, j, ws))
1165	
1166	# Octets: take and drop inside joined bytes
1167	
1168	def off.len_fast_le(+n: Nat, +xs: List<&2, B.OctByte>, h: {Nat.is_le(n, B.w8s.len.fast(xs)) == True{} : Bool}) -> {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}:
1169	  Equal.trans(Bool, Nat.is_le(n, List.length(&2, B.OctByte, xs)), Nat.is_le(n, B.w8s.len.fast(xs)), True{}, Equal.cong(Nat, Bool, k => Nat.is_le(n, k), List.length(&2, B.OctByte, xs), B.w8s.len.fast(xs), F_len(xs)), h)
1170	
1171	def off.len_fast_lt(+n: Nat, +xs: List<&2, B.OctByte>, h: {Nat.is_lt(n, B.w8s.len.fast(xs)) == True{} : Bool}) -> {Nat.is_lt(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}:
1172	  Equal.trans(Bool, Nat.is_lt(n, List.length(&2, B.OctByte, xs)), Nat.is_lt(n, B.w8s.len.fast(xs)), True{}, Equal.cong(Nat, Bool, k => Nat.is_lt(n, k), List.length(&2, B.OctByte, xs), B.w8s.len.fast(xs), F_len(xs)), h)
1173	
1174	def q_take_app_le(+n: Nat, +xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, h: {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}) -> {B.Octets{B.w8s.take.fast(n, B.w8s.append.fast(xs, ys))} == B.Octets{B.w8s.take.fast(n, xs)} : B.Octets}:
1175	  %F_app(xs, ys) : {B.Octets{B.w8s.take.fast(n, _)} == B.Octets{B.w8s.take.fast(n, xs)} : B.Octets}
1176	  %F_take(n, List.append(&2, B.OctByte, xs, ys)) : {B.Octets{_} == B.Octets{B.w8s.take.fast(n, xs)} : B.Octets}
1177	  %F_take(n, xs) : {B.Octets{B.w8s.take(n, List.append(&2, B.OctByte, xs, ys))} == B.Octets{_} : B.Octets}
1178	  Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(n, List.append(&2, B.OctByte, xs, ys)), B.w8s.take(n, xs), off.take_app_le(n, xs, ys, h))
1179	
1180	def p_take_append_le(+n: Nat, +a: B.Octets, +b: B.Octets) -> {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool} -> {B.Octets.take(n, B.Octets.append(a, b)) == B.Octets.take(n, a) : B.Octets}:
1181	  match a b:
1182	    case B.Octets{+xs} B.Octets{+ys}:
1183	      h => q_take_app_le(n, xs, ys, off.len_fast_le(n, xs, h))
1184	
1185	def p_take_append_add(+a: B.Octets, +n: Nat, +b: B.Octets) -> {B.Octets.take(Nat.add(B.Octets.len(a), n), B.Octets.append(a, b)) == B.Octets.append(a, B.Octets.take(n, b)) : B.Octets}:
1186	  match a b:
1187	    case B.Octets{+xs} B.Octets{+ys}:
1188	      %F_app(xs, ys) : {B.Octets{B.w8s.take.fast(Nat.add(B.w8s.len.fast(xs), n), _)} == B.Octets{B.w8s.append.fast(xs, B.w8s.take.fast(n, ys))} : B.Octets}
1189	      %F_len(xs) : {B.Octets{B.w8s.take.fast(Nat.add(_, n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{B.w8s.append.fast(xs, B.w8s.take.fast(n, ys))} : B.Octets}
1190	      %F_take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)) : {B.Octets{_} == B.Octets{B.w8s.append.fast(xs, B.w8s.take.fast(n, ys))} : B.Octets}
1191	      %F_take(n, ys) : {B.Octets{B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{B.w8s.append.fast(xs, _)} : B.Octets}
1192	      %F_app(xs, B.w8s.take(n, ys)) : {B.Octets{B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{_} : B.Octets}
1193	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)), List.append(&2, B.OctByte, xs, B.w8s.take(n, ys)), off.take_app_add(xs, n, ys))
1194	
1195	def q_drop_app_le(+n: Nat, +xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, h: {Nat.is_le(n, List.length(&2, B.OctByte, xs)) == True{} : Bool}) -> {B.Octets{B.w8s.drop(n, B.w8s.append.fast(xs, ys))} == B.Octets{B.w8s.append.fast(B.w8s.drop(n, xs), ys)} : B.Octets}:
1196	  %F_app(xs, ys) : {B.Octets{B.w8s.drop(n, _)} == B.Octets{B.w8s.append.fast(B.w8s.drop(n, xs), ys)} : B.Octets}
1197	  %F_app(B.w8s.drop(n, xs), ys) : {B.Octets{B.w8s.drop(n, List.append(&2, B.OctByte, xs, ys))} == B.Octets{_} : B.Octets}
1198	  Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(n, List.append(&2, B.OctByte, xs, ys)), List.append(&2, B.OctByte, B.w8s.drop(n, xs), ys), off.drop_app_le(n, xs, ys, h))
1199	
1200	def p_drop_append_le(+n: Nat, +a: B.Octets, +b: B.Octets) -> {Nat.is_le(n, B.Octets.len(a)) == True{} : Bool} -> {B.Octets.drop(n, B.Octets.append(a, b)) == B.Octets.append(B.Octets.drop(n, a), b) : B.Octets}:
1201	  match a b:
1202	    case B.Octets{+xs} B.Octets{+ys}:
1203	      h => q_drop_app_le(n, xs, ys, off.len_fast_le(n, xs, h))
1204	
1205	def p_drop_append_add(+a: B.Octets, +n: Nat, +b: B.Octets) -> {B.Octets.drop(Nat.add(B.Octets.len(a), n), B.Octets.append(a, b)) == B.Octets.drop(n, b) : B.Octets}:
1206	  match a b:
1207	    case B.Octets{+xs} B.Octets{+ys}:
1208	      %F_app(xs, ys) : {B.Octets{B.w8s.drop(Nat.add(B.w8s.len.fast(xs), n), _)} == B.Octets{B.w8s.drop(n, ys)} : B.Octets}
1209	      %F_len(xs) : {B.Octets{B.w8s.drop(Nat.add(_, n), List.append(&2, B.OctByte, xs, ys))} == B.Octets{B.w8s.drop(n, ys)} : B.Octets}
1210	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.drop(Nat.add(List.length(&2, B.OctByte, xs), n), List.append(&2, B.OctByte, xs, ys)), B.w8s.drop(n, ys), off.drop_app_add(xs, n, ys))
1211	
1212	# Octets: slices
1213	
1214	def p_slice_append_add(+a: B.Octets, +i: Nat, +n: Nat, +b: B.Octets) -> {B.Octets.slice(Nat.add(B.Octets.len(a), i), n, B.Octets.append(a, b)) == B.Octets.slice(i, n, b) : B.Octets}:
1215	  Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(Nat.add(B.Octets.len(a), i), B.Octets.append(a, b)), B.Octets.drop(i, b), p_drop_append_add(a, i, b))
1216	
1217	def p_slice_append_le(+i: Nat, +n: Nat, +a: B.Octets, +b: B.Octets, +h: {Nat.is_le(Nat.add(i, n), B.Octets.len(a)) == True{} : Bool}) -> {B.Octets.slice(i, n, B.Octets.append(a, b)) == B.Octets.slice(i, n, a) : B.Octets}:
1218	  Equal.trans(B.Octets, B.Octets.take(n, B.Octets.drop(i, B.Octets.append(a, b))), B.Octets.take(n, B.Octets.append(B.Octets.drop(i, a), b)), B.Octets.take(n, B.Octets.drop(i, a)),
1219	    Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(i, B.Octets.append(a, b)), B.Octets.append(B.Octets.drop(i, a), b), p_drop_append_le(i, a, b, off.le_add_l(i, n, B.Octets.len(a), h))),
1220	    p_take_append_le(n, B.Octets.drop(i, a), b,
1221	      Equal.trans(Bool, Nat.is_le(n, B.Octets.len(B.Octets.drop(i, a))), Nat.is_le(n, Nat.sub(B.Octets.len(a), i)), True{},
1222	        Equal.cong(Nat, Bool, k => Nat.is_le(n, k), B.Octets.len(B.Octets.drop(i, a)), Nat.sub(B.Octets.len(a), i), p_len_drop(i, a)),
1223	        off.le_sub(i, n, B.Octets.len(a), h))))
1224	
1225	def p_slice_drop(+j: Nat, +i: Nat, +n: Nat, +o: B.Octets) -> {B.Octets.slice(i, n, B.Octets.drop(j, o)) == B.Octets.slice(Nat.add(j, i), n, o) : B.Octets}:
1226	  Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(i, B.Octets.drop(j, o)), B.Octets.drop(Nat.add(j, i), o), p_drop_drop(j, i, o))
1227	
1228	def p_slice_take(+m: Nat, +i: Nat, +n: Nat, +o: B.Octets, +h: {Nat.is_le(Nat.add(i, n), m) == True{} : Bool}) -> {B.Octets.slice(i, n, B.Octets.take(m, o)) == B.Octets.slice(i, n, o) : B.Octets}:
1229	  Equal.trans(B.Octets, B.Octets.take(n, B.Octets.drop(i, B.Octets.take(m, o))), B.Octets.take(n, B.Octets.take(Nat.sub(m, i), B.Octets.drop(i, o))), B.Octets.take(n, B.Octets.drop(i, o)),
1230	    Equal.cong(B.Octets, B.Octets, x => B.Octets.take(n, x), B.Octets.drop(i, B.Octets.take(m, o)), B.Octets.take(Nat.sub(m, i), B.Octets.drop(i, o)), p_drop_take(i, m, o)),
1231	    Equal.trans(B.Octets, B.Octets.take(n, B.Octets.take(Nat.sub(m, i), B.Octets.drop(i, o))), B.Octets.take(Nat.min(n, Nat.sub(m, i)), B.Octets.drop(i, o)), B.Octets.take(n, B.Octets.drop(i, o)),
1232	      p_take_take(n, Nat.sub(m, i), B.Octets.drop(i, o)),
1233	      Equal.cong(Nat, B.Octets, k => B.Octets.take(k, B.Octets.drop(i, o)), Nat.min(n, Nat.sub(m, i)), n, off.min_le(n, Nat.sub(m, i), off.le_sub(i, n, m, h)))))
1234	
1235	# Octets: a byte at an offset
1236	
1237	def p_at_list(+o: B.Octets, +i: Nat) -> {B.Octets.at(o, i) == B.at(B.Octets.to_list(o), i) : Maybe<&2, U32>}:
1238	  match o:
1239	    case B.Octets{+ws}:
1240	      %F_to(ws) : {B.w8s.at(B.w8s.drop(i, ws)) == B.at(_, i) : Maybe<&2, U32>}
1241	      off.at_to(i, ws)
1242	
1243	def p_at_append_add(+a: B.Octets, +b: B.Octets, +i: Nat) -> {B.Octets.at(B.Octets.append(a, b), Nat.add(B.Octets.len(a), i)) == B.Octets.at(b, i) : Maybe<&2, U32>}:
1244	  match a b:
1245	    case B.Octets{+xs} B.Octets{+ys}:
1246	      %F_app(xs, ys) : {B.w8s.at(B.w8s.drop(Nat.add(B.w8s.len.fast(xs), i), _)) == B.w8s.at(B.w8s.drop(i, ys)) : Maybe<&2, U32>}
1247	      %F_len(xs) : {B.w8s.at(B.w8s.drop(Nat.add(_, i), List.append(&2, B.OctByte, xs, ys))) == B.w8s.at(B.w8s.drop(i, ys)) : Maybe<&2, U32>}
1248	      Equal.cong(List<&2, B.OctByte>, Maybe<&2, U32>, l => B.w8s.at(l), B.w8s.drop(Nat.add(List.length(&2, B.OctByte, xs), i), List.append(&2, B.OctByte, xs, ys)), B.w8s.drop(i, ys), off.drop_app_add(xs, i, ys))
1249	
1250	def q_at_app_lt(+i: Nat, +xs: List<&2, B.OctByte>, +ys: List<&2, B.OctByte>, h: {Nat.is_lt(i, List.length(&2, B.OctByte, xs)) == True{} : Bool}) -> {B.w8s.at(B.w8s.drop(i, B.w8s.append.fast(xs, ys))) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}:
1251	  %F_app(xs, ys) : {B.w8s.at(B.w8s.drop(i, _)) == B.w8s.at(B.w8s.drop(i, xs)) : Maybe<&2, U32>}
1252	  off.at_app_lt(i, xs, ys, h)
1253	
1254	def p_at_append_lt(+a: B.Octets, +b: B.Octets, +i: Nat) -> {Nat.is_lt(i, B.Octets.len(a)) == True{} : Bool} -> {B.Octets.at(B.Octets.append(a, b), i) == B.Octets.at(a, i) : Maybe<&2, U32>}:
1255	  match a b:
1256	    case B.Octets{+xs} B.Octets{+ys}:
1257	      h => q_at_app_lt(i, xs, ys, off.len_fast_lt(i, xs, h))
1258	
1259	def p_at_drop(+j: Nat, +o: B.Octets, +i: Nat) -> {B.Octets.at(B.Octets.drop(j, o), i) == B.Octets.at(o, Nat.add(j, i)) : Maybe<&2, U32>}:
1260	  match o:
1261	    case B.Octets{+ws}:
1262	      Equal.cong(List<&2, B.OctByte>, Maybe<&2, U32>, l => B.w8s.at(l), B.w8s.drop(i, B.w8s.drop(j, ws)), B.w8s.drop(Nat.add(j, i), ws), off.drop_drop(j, i, ws))
1263	
1264	def p_at_take(+n: Nat, +o: B.Octets, +i: Nat, h: {Nat.is_lt(i, n) == True{} : Bool}) -> {B.Octets.at(B.Octets.take(n, o), i) == B.Octets.at(o, i) : Maybe<&2, U32>}:
1265	  match o:
1266	    case B.Octets{+ws}:
1267	      %F_take(n, ws) : {B.w8s.at(B.w8s.drop(i, _)) == B.w8s.at(B.w8s.drop(i, ws)) : Maybe<&2, U32>}
1268	      off.at_take(i, n, ws, h)
1269	
1270	# Every word ANDed with zero is zero (for low16_mask)
1271	
1272	def off.band_f(+b: Bool) -> {Bool.and(b, False{}) == False{} : Bool}:
1273	  match b:
1274	    case True{}:
1275	      {==}
1276	    case False{}:
1277	      {==}
1278	
1279	def off.wand_zero(+n: Nat, w: Word(n)) -> {Word.and(n, w, Word.zero(n)) == Word.zero(n) : Word(n)}:
1280	  match n:
1281	    case 0n:
1282	      {==}
1283	    case 1n+p:
1284	      match w:
1285	        case WCon{+b, t}:
1286	          %Equal.sym(Bool, Bool.and(b, False{}), False{}, off.band_f(b)) : {WCon{_, Word.and(p, t, Word.zero(p))} == Word.zero(1n+p) : Word(1n+p)}
1287	          Equal.cong(Word(p), Word(1n+p), z => WCon{False{}, z}, Word.and(p, t, Word.zero(p)), Word.zero(p), off.wand_zero(p, t))
1288	
1289	# The laws
1290	
1291	def Laws.octets_len_append(a, b):
1292	  p_len_append(a, b)
1293	
1294	def Laws.octets_len_take(n, o):
1295	  p_len_take(n, o)
1296	
1297	def Laws.octets_len_take_le(n, o, h):
1298	  p_len_take_le(n, o, h)
1299	
1300	def Laws.octets_len_drop(n, o):
1301	  p_len_drop(n, o)
1302	
1303	def Laws.octets_len_slice(i, n, o):
1304	  p_len_slice(i, n, o)
1305	
1306	def Laws.octets_len_slice_le(i, n, o, h):
1307	  p_len_slice_le(i, n, o, h)
1308	
1309	def Laws.octets_len_zeros(n):
1310	  p_len_zeros(n)
1311	
1312	def Laws.octets_len_of_list(xs):
1313	  p_len_of_list(xs)
1314	
1315	def Laws.octets_append_assoc(a, b, c):
1316	  p_append_assoc(a, b, c)
1317	
1318	def p_append_empty_l(+o: B.Octets) -> {B.Octets.append(B.Octets.empty(), o) == o : B.Octets}:
1319	  match o:
1320	    case B.Octets{+ws}:
1321	      %F_app(Nil{}, ws) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1322	      {==}
1323	
1324	def p_append_empty_r(+o: B.Octets) -> {B.Octets.append(o, B.Octets.empty()) == o : B.Octets}:
1325	  match o:
1326	    case B.Octets{+ws}:
1327	      %F_app(ws, Nil{}) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1328	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, List.append(&2, B.OctByte, ws, Nil{}), ws, app_nil8(ws))
1329	
1330	def off.take_len(ws: List<&2, B.OctByte>) -> {B.w8s.take(List.length(&2, B.OctByte, ws), ws) == ws : List<&2, B.OctByte>}:
1331	  match ws:
1332	    case Nil{}:
1333	      {==}
1334	    case Con{h, t}:
1335	      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, B.w8s.take(List.length(&2, B.OctByte, t), t), t, off.take_len(t))
1336	
1337	def p_take_len(+o: B.Octets) -> {B.Octets.take(B.Octets.len(o), o) == o : B.Octets}:
1338	  match o:
1339	    case B.Octets{+ws}:
1340	      %F_take(B.w8s.len.fast(ws), ws) : {B.Octets{_} == B.Octets{ws} : B.Octets}
1341	      %F_len(ws) : {B.Octets{B.w8s.take(_, ws)} == B.Octets{ws} : B.Octets}
1342	      Equal.cong(List<&2, B.OctByte>, B.Octets, l => B.Octets{l}, B.w8s.take(List.length(&2, B.OctByte, ws), ws), ws, off.take_len(ws))
1343	
1344	def Laws.octets_drop_zero(o):
1345	  match o:
1346	    case B.Octets{ws}:
1347	      {==}
1348	
1349	def Laws.octets_take_len(o):
1350	  p_take_len(o)
1351	
1352	def Laws.octets_append_empty_l(o):
1353	  p_append_empty_l(o)
1354	
1355	def Laws.octets_append_empty_r(o):
1356	  p_append_empty_r(o)
1357	
1358	def Laws.octets_drop_drop(j, i, o):
1359	  p_drop_drop(j, i, o)
1360	
1361	def Laws.octets_take_take(i, j, o):
1362	  p_take_take(i, j, o)
1363	
1364	def Laws.octets_take_drop_comm(i, j, o):
1365	  p_take_drop(i, j, o)
1366	
1367	def Laws.octets_drop_take_comm(i, j, o):
1368	  p_drop_take(i, j, o)
1369	
1370	def Laws.octets_take_append_le(n, a, b, h):
1371	  p_take_append_le(n, a, b, h)
1372	
1373	def Laws.octets_take_append_add(a, n, b):
1374	  p_take_append_add(a, n, b)
1375	
1376	def Laws.octets_drop_append_le(n, a, b, h):
1377	  p_drop_append_le(n, a, b, h)
1378	
1379	def Laws.octets_drop_append_add(a, n, b):
1380	  p_drop_append_add(a, n, b)
1381	
1382	def Laws.octets_slice_append_add(a, i, n, b):
1383	  p_slice_append_add(a, i, n, b)
1384	
1385	def Laws.octets_slice_append_le(i, n, a, b, h):
1386	  p_slice_append_le(i, n, a, b, h)
1387	
1388	def Laws.octets_slice_drop(j, i, n, o):
1389	  p_slice_drop(j, i, n, o)
1390	
1391	def Laws.octets_slice_take(m, i, n, o, h):
1392	  p_slice_take(m, i, n, o, h)
1393	
1394	def Laws.octets_at_list(o, i):
1395	  p_at_list(o, i)
1396	
1397	def Laws.octets_at_append_add(a, b, i):
1398	  p_at_append_add(a, b, i)
1399	
1400	def Laws.octets_at_append_lt(a, b, i, h):
1401	  p_at_append_lt(a, b, i, h)
1402	
1403	def Laws.octets_at_drop(j, o, i):
1404	  p_at_drop(j, o, i)
1405	
1406	def Laws.octets_at_take(n, o, i, h):
1407	  p_at_take(n, o, i, h)
1408	
1409	def Laws.at_append_add(a, b, i):
1410	  Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.at.head(l), B.drop(Nat.add(B.len(a), i), B.append(a, b)), B.drop(i, b), off.ldrop_app_add(a, i, b))
1411	
1412	def Laws.at_append_lt(a, b, i, h):
1413	  off.lat_app_lt(i, a, b, h)
1414	
1415	def Laws.at_drop(j, xs, i):
1416	  Equal.cong(List<&2, U32>, Maybe<&2, U32>, l => B.at.head(l), B.drop(i, B.drop(j, xs)), B.drop(Nat.add(j, i), xs), off.ldrop_drop(j, i, xs))
1417	
1418	def Laws.at_take(n, xs, i, h):
1419	  off.lat_take(i, n, xs, h)
1420	
1421	def Laws.octets_len_le16(v):
1422	  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.le16(v))), B.len(B.le16(v)), 2n, p_len_of_list(B.le16(v)), off.llen_le16(v))
1423	
1424	def Laws.octets_len_be16(v):
1425	  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.be16(v))), B.len(B.be16(v)), 2n, p_len_of_list(B.be16(v)), off.llen_be16(v))
1426	
1427	def Laws.octets_len_le32(v):
1428	  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.le32(v))), B.len(B.le32(v)), 4n, p_len_of_list(B.le32(v)), off.llen_le32(v))
1429	
1430	def Laws.octets_len_be32(v):
1431	  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.be32(v))), B.len(B.be32(v)), 4n, p_len_of_list(B.be32(v)), off.llen_be32(v))
1432	
1433	def Laws.octets_len_le64(v):
1434	  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.le64(v))), B.len(B.le64(v)), 8n, p_len_of_list(B.le64(v)), off.llen_le64(v))
1435	
1436	def Laws.octets_len_be64(v):
1437	  Equal.trans(Nat, B.Octets.len(B.Octets.of_list(B.be64(v))), B.len(B.be64(v)), 8n, p_len_of_list(B.be64(v)), off.llen_be64(v))
1438	
1439	def Laws.octets_le16_at_append_add(a, b, i):
1440	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, b), p_slice_append_add(a, i, 2n, b))
1441	
1442	def Laws.octets_le16_at_append_le(a, b, i, h):
1443	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, a), p_slice_append_le(i, 2n, a, b, h))
1444	
1445	def Laws.octets_le16_at_drop(j, o, i):
1446	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 2n, o), p_slice_drop(j, i, 2n, o))
1447	
1448	def Laws.octets_le16_at_take(n, o, i, h):
1449	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.take(n, o)), B.Octets.slice(i, 2n, o), p_slice_take(n, i, 2n, o, h))
1450	
1451	def Laws.octets_be16_at_append_add(a, b, i):
1452	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, b), p_slice_append_add(a, i, 2n, b))
1453	
1454	def Laws.octets_be16_at_append_le(a, b, i, h):
1455	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.append(a, b)), B.Octets.slice(i, 2n, a), p_slice_append_le(i, 2n, a, b, h))
1456	
1457	def Laws.octets_be16_at_drop(j, o, i):
1458	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 2n, o), p_slice_drop(j, i, 2n, o))
1459	
1460	def Laws.octets_be16_at_take(n, o, i, h):
1461	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be16.head(B.Octets.to_list(s)), B.Octets.slice(i, 2n, B.Octets.take(n, o)), B.Octets.slice(i, 2n, o), p_slice_take(n, i, 2n, o, h))
1462	
1463	def Laws.octets_le32_at_append_add(a, b, i):
1464	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, b), p_slice_append_add(a, i, 4n, b))
1465	
1466	def Laws.octets_le32_at_append_le(a, b, i, h):
1467	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, a), p_slice_append_le(i, 4n, a, b, h))
1468	
1469	def Laws.octets_le32_at_drop(j, o, i):
1470	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 4n, o), p_slice_drop(j, i, 4n, o))
1471	
1472	def Laws.octets_le32_at_take(n, o, i, h):
1473	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.le32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.take(n, o)), B.Octets.slice(i, 4n, o), p_slice_take(n, i, 4n, o, h))
1474	
1475	def Laws.octets_be32_at_append_add(a, b, i):
1476	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(Nat.add(B.Octets.len(a), i), 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, b), p_slice_append_add(a, i, 4n, b))
1477	
1478	def Laws.octets_be32_at_append_le(a, b, i, h):
1479	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.append(a, b)), B.Octets.slice(i, 4n, a), p_slice_append_le(i, 4n, a, b, h))
1480	
1481	def Laws.octets_be32_at_drop(j, o, i):
1482	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 4n, o), p_slice_drop(j, i, 4n, o))
1483	
1484	def Laws.octets_be32_at_take(n, o, i, h):
1485	  Equal.cong(B.Octets, Maybe<&2, U32>, s => B.be32.head(B.Octets.to_list(s)), B.Octets.slice(i, 4n, B.Octets.take(n, o)), B.Octets.slice(i, 4n, o), p_slice_take(n, i, 4n, o, h))
1486	
1487	def Laws.octets_le64_at_append_add(a, b, i):
1488	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(Nat.add(B.Octets.len(a), i), 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, b), p_slice_append_add(a, i, 8n, b))
1489	
1490	def Laws.octets_le64_at_append_le(a, b, i, h):
1491	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, a), p_slice_append_le(i, 8n, a, b, h))
1492	
1493	def Laws.octets_le64_at_drop(j, o, i):
1494	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 8n, o), p_slice_drop(j, i, 8n, o))
1495	
1496	def Laws.octets_le64_at_take(n, o, i, h):
1497	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.le64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.take(n, o)), B.Octets.slice(i, 8n, o), p_slice_take(n, i, 8n, o, h))
1498	
1499	def Laws.octets_be64_at_append_add(a, b, i):
1500	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(Nat.add(B.Octets.len(a), i), 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, b), p_slice_append_add(a, i, 8n, b))
1501	
1502	def Laws.octets_be64_at_append_le(a, b, i, h):
1503	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.append(a, b)), B.Octets.slice(i, 8n, a), p_slice_append_le(i, 8n, a, b, h))
1504	
1505	def Laws.octets_be64_at_drop(j, o, i):
1506	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.drop(j, o)), B.Octets.slice(Nat.add(j, i), 8n, o), p_slice_drop(j, i, 8n, o))
1507	
1508	def Laws.octets_be64_at_take(n, o, i, h):
1509	  Equal.cong(B.Octets, Maybe<&2, W.W64>, s => B.be64_at(B.Octets.to_list(s), 0n), B.Octets.slice(i, 8n, B.Octets.take(n, o)), B.Octets.slice(i, 8n, o), p_slice_take(n, i, 8n, o, h))
1510	
1511	def Laws.low16_mask(v):
1512	  match v:
1513	    case U32{WCon{x0, WCon{x1, WCon{x2, WCon{x3, WCon{x4, WCon{x5, WCon{x6, WCon{x7, WCon{x8, WCon{x9, WCon{x10, WCon{x11, WCon{x12, WCon{x13, WCon{x14, WCon{x15, t}}}}}}}}}}}}}}}}}:
1514	      Equal.cong(Word(16n), U32, z => U32{WCon{Bool.and(x0, True{}), WCon{Bool.and(x1, True{}), WCon{Bool.and(x2, True{}), WCon{Bool.and(x3, True{}), WCon{Bool.and(x4, True{}), WCon{Bool.and(x5, True{}), WCon{Bool.and(x6, True{}), WCon{Bool.and(x7, True{}), WCon{Bool.and(x8, True{}), WCon{Bool.and(x9, True{}), WCon{Bool.and(x10, True{}), WCon{Bool.and(x11, True{}), WCon{Bool.and(x12, True{}), WCon{Bool.and(x13, True{}), WCon{Bool.and(x14, True{}), WCon{Bool.and(x15, True{}), z}}}}}}}}}}}}}}}}}, Word.zero(16n), Word.and(16n, t, Word.zero(16n)), Equal.sym(Word(16n), Word.and(16n, t, Word.zero(16n)), Word.zero(16n), off.wand_zero(16n, t)))