proposition: Lemma remove_all_belongs : forall x xs F, ¬ List.In x xs -> (x :: xs) ⊂ F -> xs ⊂ (F ∖ {x}).
proof: Proof. intros x xs F Hnotin Hincl. unfold all_belongs in *. intros y Hin. simpl in *. apply belongs_remove; auto. intro; subst. contradiction. Qed.
imports: Utf8 Equalities