proposition: Lemma StronglySorted_restr A cond (r: relation A) l: StronglySorted (restr_rel cond r) l -> StronglySorted r l.
proof: Proof. induction l; ins; vauto. rewrite StronglySorted_cons_iff, ForallE in *. firstorder. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid