proposition: Lemma get_single_eq_inv : forall x y v w, get x (y ∶ w) = Some v -> x = y /\ v = w.
proof: Proof. intros x y v w Hget. simpl in Hget. destruct (eq_keys_dec x y) as [ Heq | Hneq ]; subst; inversion Hget; auto. Qed.
imports: Utf8 Equalities