proposition: Lemma notin_concat_inv : forall x F G, x ∉ (F & G) -> x ∉ F ∧ x ∉ G.
proof: Proof. intros x F G Hnotin. split; intro Hin; elim Hnotin; [ apply belongs_concat_l | apply belongs_concat_r ]; auto. Qed.
imports: Utf8 Equalities