proposition: Lemma notin_concat : forall x F G, x ∉ F -> x ∉ G -> x ∉ (F & G).
proof: Proof. intros x F G HnotinF HnotinG HinFG. apply belongs_concat_inv in HinFG. destruct HinFG; [ elim HnotinF | elim HnotinG ]; auto. Qed.
imports: Utf8 Equalities