proposition: Lemma subset_subset_union : forall s1 s2 s, subset s1 s -> subset s2 s -> subset (union s1 s2) s.
proof: Proof. intros s1 s2 s H1 H2 e H. destruct (union_12 _ _ _ H); [ apply H1 | apply H2]; trivial. Qed.
imports: List more_list list_permut Arith