proposition: Lemma not_elem_of_app_cons_inv_r x y l1 l2 k1 k2 : x ∉ k2 → y ∉ l2 → l1 ++ x :: l2 = k1 ++ y :: k2 → l1 = k1 ∧ x = y ∧ l2 = k2.
proof: Proof. intros. destruct (not_elem_of_app_cons_inv_l x y (reverse l2) (reverse l1) (reverse k2) (reverse k1)); [..|naive_solver]. - by rewrite elem_of_reverse. - by rewrite elem_of_reverse. - rewrite <-!reverse_snoc, <-!reverse_app, <-!(assoc_L (++)). by f_equal. Qed.
imports: stdpp(options)