proposition: Lemma all_notin_update : forall xs E F, xs ⊄ E -> xs ⊄ (E ::= F).
proof: Proof. intros xs E F Hnotincl. unfold all_notin in *. intros x Hin. apply Hnotincl in Hin. apply notin_update; auto. Qed.
imports: Utf8 Equalities