law zip_nil_left

bend-mathlib@0.8.1.0 · list.bend:1608

import Base

1608# Zipping the empty list with anything gives the empty list.
1609law zip_nil_left:
1610  for -a: Quant
1611  for -A: Kind(a)
1612  for -b: Quant
1613  for -B: Kind(b)
1614  for -ys: List<b, B>
1615  {List.zip(a, A, b, B, Nil{}, ys) == Nil{} : List<&1, A & B>}