proposition: Lemma get_concat_r : forall x y v E, x = y -> get x (E & (y ∶ v)) = Some v.
proof: Proof. intros x y v E Heq; subst. simpl. assert (y = y) by auto. destruct (eq_keys_dec y y); auto; try contradiction. Qed.
imports: Utf8 Equalities