law length_zip_sym

bend-mathlib@0.8.1.0 · list.bend:2415

import Base

2415# A zip is as long as the shorter of the two lists, reversed to rewrite toward the simple side.
2416law length_zip_sym:
2417  for -a: Quant
2418  for -A: Kind(a)
2419  for xs: List<a, A>
2420  for ys: List<a, A>
2421  {Nat.min(List.length(a, A, xs), List.length(a, A, ys)) == List.length(&1, A & A, List.zip(a, A, a, A, xs, ys)) : Nat}