proposition: Lemma Permutation_filterP2 A f f' (EQ: f ≡₁ f') l l' (P: Permutation (A:=A) l l') : Permutation (filterP f l) (filterP f' l').
proof: Proof. replace (filterP f' l') with (filterP f l'); auto using Permutation_filterP, filterP_set_equiv. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation