proposition: Lemma remove_belongs_concat_r : forall x E F, x ∈ F -> (E & F) ∖ {x} = E & (F ∖ {x}).
proof: Proof. intros x E F Hin. induction F as [ | (y, v) F IHF ]; simpl; auto. inversion Hin. assert (x ∈ F & (y ∶ v)) as Hin2 by auto. clear Hin. apply belongs_concat_inv in Hin2. destruct Hin2 as [ Hin | Hin ]. apply IHF in Hin. rewrite Hin. destruct (eq_keys_dec x y); subst; auto. apply belongs_single_inv in Hin; subst. rewrite ?eq_keys_true; auto. Qed.
imports: Utf8 Equalities