law zip_nil_right_sym

bend-mathlib@0.8.1.0 · list.bend:2857

import Base

2857# Zipping anything with the empty list gives the empty list, reversed to rewrite toward the simple side.
2858law zip_nil_right_sym:
2859  for -a: Quant
2860  for -A: Kind(a)
2861  for -b: Quant
2862  for -B: Kind(b)
2863  for xs: List<a, A>
2864  {Nil{} == List.zip(a, A, b, B, xs, Nil{}) : List<&1, A & B>}