proposition: Lemma all_remove_belongs_concat_r : forall xs E F, List.NoDup xs -> xs ⊂ F -> (E & F) ∖ xs = E & (F ∖ xs).
proof: Proof. induction xs as [ | x xs IHxs ]; intros E F Hnodup Hincl; simpl; auto. inversion Hnodup. rewrite remove_belongs_concat_r; auto. rewrite IHxs; auto. apply remove_all_belongs; auto. apply all_belongs_belongs in Hincl. destruct Hincl; auto. Qed.
imports: Utf8 Equalities