proposition: Lemma not_elem_of_app_cons_inv_l x y l1 l2 k1 k2 : x ∉ k1 → y ∉ l1 → l1 ++ x :: l2 = k1 ++ y :: k2 → l1 = k1 ∧ x = y ∧ l2 = k2.
proof: Proof. revert k1. induction l1 as [|x' l1 IH]; intros [|y' k1] Hx Hy ?; simplify_eq/=; try apply not_elem_of_cons in Hx as [??]; try apply not_elem_of_cons in Hy as [??]; naive_solver. Qed.
imports: stdpp(options)