proposition: Lemma filter_app A f (l l' : list A) : filter f (l ++ l') = filter f l ++ filter f l'.
proof: Proof. induction l; ins; desf; ins; congruence. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation