proposition: Lemma belongs_update_one_inv : forall x y v E, y ∈ (E [x <- v]) -> y ∈ E.
proof: Proof. intros x y v. induction E as [ | (z, w) E IHE ]; intro Hin; simpl in *; auto. destruct (eq_keys_dec x z) as [ Heq | Hneq ]; simpl in *; auto. unfold belongs in Hin |- *. simpl in *. destruct Hin; [ left | right ]; auto. apply IHE; auto. Qed.
imports: Utf8 Equalities