proposition: Lemma subset_dec : forall s1 s2, {subset s1 s2} + {~ subset s1 s2}.
proof: Proof. intros [l1 wr1]; induction l1 as [ | e1 l1]; intros [l2 wr2]. left; intro e; contradiction. destruct (In_dec eq_elt_dec e1 l2) as [ e1_in_l2 | e1_not_in_l2 ]. assert (wr1' := without_red_remove e1 nil l1 wr1); simpl in wr1'. destruct (IHl1 wr1' (mk_set l2 wr2)) as [ s1_incl_s2 | s1_not_incl_s2 ]. left; intros e [e_eq_e1 | e_in_l1]; [subst | apply s1_incl_s2]; trivial. right; intro H; apply s1_not_incl_s2; intros e e_in_l1; apply H; right; trivial. right; intro H; apply e1_not_in_l2; apply H; left; trivial. Qed.
imports: List more_list list_permut Arith