proposition: Lemma union_compat_subset : forall s1 s2 s1' s2', subset s1 s2 -> subset s1' s2' -> subset (union s1 s1') (union s2 s2').
proof: Proof. intros [l1 wr1] [l2 wr2] [l1' wr1'] [l2' wr2']; unfold subset; simpl; intros H H' e e_in_ll1. generalize (union_12_aux _ _ _ e_in_ll1); intros [ e_in_l1 | e_in_l1']. apply union_1; apply H; trivial. apply union_2; apply H'; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)