proposition: Lemma in_concat A (a: A) l ll : In a l -> In l ll -> In a (concat ll).
proof: Proof. rewrite in_concat_iff; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation