law zip_nil_right

bend-mathlib@0.8.1.0 · list.bend:1620

import Base

1620# Zipping anything with the empty list gives the empty list.
1621law zip_nil_right:
1622  for -a: Quant
1623  for -A: Kind(a)
1624  for -b: Quant
1625  for -B: Kind(b)
1626  for xs: List<a, A>
1627  {List.zip(a, A, b, B, xs, Nil{}) == Nil{} : List<&1, A & B>}