proposition: Lemma prefix_not_elem_of_app_cons_inv x y l1 l2 k1 k2 : x ∉ k1 → y ∉ l1 → (l1 ++ x :: l2) `prefix_of` (k1 ++ y :: k2) → l1 = k1 ∧ x = y ∧ l2 `prefix_of` k2.
proof: Proof. intros Hin1 Hin2 [k Hle]. rewrite <-(assoc_L (++)) in Hle. apply not_elem_of_app_cons_inv_l in Hle; [|done..]. unfold prefix. naive_solver. Qed.
imports: stdpp(options)