proposition: Lemma Permutation_filterP A (l l' : list A) (P: Permutation l l') f : Permutation (filterP f l) (filterP f l').
proof: Proof. induction P; ins; desf; vauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation