law is_empty_map_sym

bend-mathlib@0.8.1.0 · list.bend:3034

import Base

3034# A map is empty exactly when the list is, reversed to rewrite toward the simple side.
3035law is_empty_map_sym:
3036  for ~A: Type
3037  for ~B: Type
3038  for ~f: A -> B
3039  for xs: List<A>
3040  {List.is_empty(&1, A, xs) == List.is_empty(&1, B, List.map(~A, ~B, ~f, xs)) : Bool}