proposition: Lemma remove_update_eq : forall x y v E, x = y -> (E ::= (y ∶ v)) ∖ {x} = E ∖ {x}.
proof: Proof. intros; subst. induction E as [ | (y', v') ]; simpl; auto. destruct (eq_keys_dec y y'); subst; simpl. rewrite eq_keys_true; auto. rewrite eq_keys_false; auto. f_equal; auto. Qed.
imports: Utf8 Equalities