proposition: Lemma all_remove_single_in : forall x xs v, List.In x xs -> (x ∶ v) ∖ xs = (@empty A).
proof: Proof. intros x xs v; induction xs as [ | y ]; intros Hin; simpl in *; auto; inversion Hin; subst. rewrite eq_keys_true. apply all_remove_empty. destruct (eq_keys_dec y x). apply all_remove_empty. auto. Qed.
imports: Utf8 Equalities