proposition: Lemma all_notin_update_one : forall x xs v E, xs ⊄ E -> xs ⊄ (E [x <- v]).
proof: Proof. intros x xs v E Hnotin. unfold all_notin in *. intros y Hin. apply Hnotin in Hin. apply notin_update_one; auto. Qed.
imports: Utf8 Equalities