proposition: Lemma update_one_single : forall x y v w, x = y -> (x ∶ v) [y <- w] = (x ∶ w).
proof: Proof. intros x y v w Heq. subst. simpl. destruct (eq_keys_dec y y) as [ Heq | Hneq ]; auto; elim Hneq; auto. Qed.
imports: Utf8 Equalities