proposition: Lemma notin_update_one : forall x y v E, y ∉ E -> y ∉ (E [x <- v]).
proof: Proof. intros x y v E Hnotin. unfold notin in *. intro Hin. elim Hnotin. apply belongs_update_one_inv with x v; auto. Qed.
imports: Utf8 Equalities