proposition: Lemma remove_belongs_concat_l : forall x E F, x ∉ F -> (E & F) ∖ {x} = (E ∖ {x}) & F.
proof: Proof. intros x E F Hnotin. induction F as [ | (y, v) F IHF ]; simpl; auto. assert (x ∉ F & (y ∶ v)) as Hnotin2 by auto. clear Hnotin. apply notin_concat_inv in Hnotin2. destruct Hnotin2 as [ Hnotin Hnotin2 ]. apply IHF in Hnotin. rewrite Hnotin. destruct (eq_keys_dec x y); subst; auto. apply notin_single_inv in Hnotin2. elim Hnotin2; auto. Qed.
imports: Utf8 Equalities