proposition: Lemma all_remove_single_not_in : forall x xs v, ¬ List.In x xs -> (x ∶ v) ∖ xs = (x ∶ v).
proof: Proof. intros x xs v Hnotin. induction xs as [ | y xs IHxs ]; simpl; auto. assert (x ≠ y ∧ ¬In x xs) as Hyp by (split; intro Hyp; apply Hnotin; [ rewrite Hyp; apply in_eq | apply in_cons; auto ]). destruct Hyp as [ Hneq Hnotin2 ]. apply IHxs in Hnotin2. rewrite <- Hnotin2. f_equal. apply eq_keys_false; auto. Qed.
imports: Utf8 Equalities