proposition: Lemma all_remove_belongs_concat_l : forall xs E F, xs ⊄ F -> (E & F) ∖ xs = (E ∖ xs) & F.
proof: Proof. induction xs as [ | x ]; intros E F Hnotincl; simpl; auto. apply all_notin_notin in Hnotincl. destruct Hnotincl. rewrite remove_belongs_concat_l; auto. Qed.
imports: Utf8 Equalities