proposition: Lemma elem_of_StronglySorted_app l1 l2 x1 x2 : StronglySorted R (l1 ++ l2) → x1 ∈ l1 → x2 ∈ l2 → R x1 x2.
proof: Proof. induction l1 as [|x1' l1 IH]; simpl; [by rewrite elem_of_nil|]. intros [? Hall]%StronglySorted_inv [->|?]%elem_of_cons ?; [|by auto]. rewrite Forall_app, !Forall_forall in Hall. naive_solver. Qed.
imports: stdpp(options)