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