proposition: Lemma StronglySorted_app_iff A (r: relation A) l1 l2 : StronglySorted r (l1 ++ l2) <-> StronglySorted r l1 /\ StronglySorted r l2 /\ (forall x1 (IN1: In x1 l1) x2 (IN2: In x2 l2), r x1 x2).
proof: Proof. induction l1; ins; [by intuition; vauto|]. rewrite !StronglySorted_cons_iff, IHl1, Forall_app. clear; intuition; desf; eauto. all: rewrite Forall_forall in *; eauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid