proposition: Lemma NoDup_app l k : NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
proof: Proof. induction l; simpl. - rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver. - rewrite !NoDup_cons. setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver. Qed.
imports: stdpp(options)