law length_map

bend-mathlib@0.8.1.0 · list.bend:178

import Base

178# Mapping preserves the length.
179law length_map:
180  for ~A: Type
181  for ~B: Type
182  for ~f: A -> B
183  for xs: List<A>
184  {List.length(&1, B, List.map(~A, ~B, ~f, xs)) == List.length(&1, A, xs) : Nat}