law length_map_sym

bend-mathlib@0.8.1.0 · list.bend:2238

import Base

2238# Mapping preserves the length, reversed to rewrite toward the simple side.
2239law length_map_sym:
2240  for ~A: Type
2241  for ~B: Type
2242  for ~f: A -> B
2243  for xs: List<A>
2244  {List.length(&1, A, xs) == List.length(&1, B, List.map(~A, ~B, ~f, xs)) : Nat}