>>50226377another fix:
forall f : list bool -> list bool,
(forall x y, f x = f y -> x = y) ->
forall n : nat,
forall ls : list (list bool),
(forall l : list bool, length l <= n <-> In l ls) ->
NoDup ls ->
length (flat_map f ls) >= length (flat_map id ls)