proposition: Lemma all_remove_singles_in : forall xs ys vs, xs = ys -> length xs = length vs -> (xs ∷ vs) ∖ ys = (@empty A).
proof: Proof. intros xs vs ys Heq; subst. generalize vs. clear vs. induction ys as [ | y ]; induction vs as [ | v ]; intro Hlen; simpl in *; auto. inversion Hlen. rewrite eq_keys_true; auto. Qed.
imports: Utf8 Equalities