proposition: Lemma all_remove_ok_notin : forall xs E, ok E -> xs ⊄ (E ∖ xs).
proof: Proof. induction xs as [ | x xs IHxs ]; intros E Hok; simpl. unfold all_notin. intros x Hin. inversion Hin. apply notin_all_notin. split. apply notin_all_remove_notin. apply remove_ok_notin; auto. apply IHxs. apply ok_remove; auto. Qed.
imports: Utf8 Equalities