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