proposition: Lemma in_concat_fst A a (l : list A) B (l' : list B) ll : In (l, l') ll -> In a l -> In a (concat (map fst ll)).
proof: Proof. ins; rewrite <- flat_map_concat_map, in_flat_map; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation