proposition: Lemma update_one_notin : forall x v E, x ∉ E -> E [x <- v] = E.
proof: Proof. intros x v E Hnotin. induction E as [ | (y, w) E IHE ]; simpl in *; auto. destruct (eq_keys_dec x y) as [ Heq | Hneq ]; subst; simpl in *; auto. unfold notin in Hnotin. unfold belongs in Hnotin. simpl in Hnotin. elim Hnotin; auto. f_equal; apply IHE. assert (x ∉ (E & (y ∶ w))) as Hnotin2 by auto. apply notin_concat_inv in Hnotin2. destruct Hnotin2; auto. Qed.
imports: Utf8 Equalities