proposition: Lemma StronglySorted_app A (r: relation A) l1 l2 (S1: StronglySorted r l1) (S2: StronglySorted r l2) (L: forall x1 (IN1: In x1 l1) x2 (IN2: In x2 l2), r x1 x2): StronglySorted r (l1 ++ l2).
proof: Proof. by apply StronglySorted_app_iff. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnEquational Sorted Setoid