proposition: Lemma Forall_filterP A (P: A -> Prop) f l : Forall P l -> Forall P (filterP f l).
proof: Proof. rewrite !Forall_forall; ins. rewrite in_filterP_iff in H0; desf; eauto. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation