proposition: Lemma StronglySorted_filterP A r f (l : list A): StronglySorted r l -> StronglySorted r (filterP f l).
proof: Proof. induction l; ins; eauto; desf; rewrite StronglySorted_cons_iff in *; desf. all: splits; desf; eauto using Forall_filterP. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid