proposition: Lemma rev_filterP A f (l : list A) : rev (filterP f l) = filterP f (rev l).
proof: Proof. induction l; ins; desf; ins; rewrite filterP_app, IHl; ins; desf; ins. auto using app_nil_end. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation