proposition: Lemma all_belongs_concat_r : forall xs F G, xs ⊂ F -> xs ⊂ (G & F).
proof: Proof. intros xs F G Hincl. unfold all_belongs in *. intros x Hin. apply Hincl in Hin. apply belongs_concat_r; auto. Qed.
imports: Utf8 Equalities