proposition: Lemma get_concat_inv : forall x y v w E, get x (E & (y ∶ v)) = Some w -> (x = y /\ v = w) \/ (x <> y /\ get x E = Some w).
proof: Proof. intros x y v w E Hget. simpl in *. destruct (eq_keys_dec x y); [ left | right ]; inversion Hget; auto. Qed.
imports: Utf8 Equalities