law is_empty_map

bend-mathlib@0.8.1.0 · list.bend:1885

import Base

1885# A map is empty exactly when the list is.
1886law is_empty_map:
1887  for ~A: Type
1888  for ~B: Type
1889  for ~f: A -> B
1890  for xs: List<A>
1891  {List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) == List.is_empty(&1, A, xs) : Bool}