proposition: Lemma StronglySorted_cons_iff A (r : relation A) (a : A) (l : list A) : StronglySorted r (a :: l) <-> StronglySorted r l /\ Forall (r a) l.
proof: Proof. split; ins; desf; auto using SSorted_cons, StronglySorted_inv. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid