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