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