law lists_end

lawful-bytes@0.1.1.0 · proof_same.bend:410

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

410# Comparing n more bytes from i of A and from j of B, after an empty prefix:
411# acc and the comparison of the two slices.
412law lists_end:
413  for +acc: Bool
414  for +xs: List<&2, U32>
415  for +ys: List<&2, U32>
416  {acc == Bool.and(acc, D.list_eq(List.take(&2, U32, xs, 0n), List.take(&2, U32, ys, 0n))) : Bool}