proposition: Lemma union_compat_subset_1 : forall s1 s2 s, subset s1 s2 -> subset (union s1 s) (union s2 s).
proof: Proof. intros [l1 wr1] [l2 wr2] [l wr]; unfold subset; simpl; intros H e e_in_ll1. generalize (union_12_aux _ _ _ e_in_ll1); intros [ e_in_l | e_in_l1]; trivial. apply union_1; apply H; trivial. apply union_2; trivial. Qed.
imports: List more_list list_permut Arith