proposition: Lemma subset_dec : forall s1 s2, {subset s1 s2} + {~ subset s1 s2}.
proof: Proof. unfold subset, mem; intros s1 s2; case s1; clear s1; simpl; intros l1 _; case s2; clear s2; simpl; intros l2 _. revert l1 l2; fix subset_dec 1. intros l1; case l1; clear l1; simpl. intros l2; left; intros; contradiction. intros a1 l1 l2. generalize (mem_bool_ok _ _ eq_bool_ok a1 l2); case (mem_bool eq_bool a1 l2). intro a1_in_l2; case (subset_dec l1 l2). intros l1_in_l2; left. intros e e_in_a1l1; case e_in_a1l1; clear e_in_a1l1. intro e_eq_a1; apply (mem_eq_mem eq_proof a1). apply (equiv_sym _ _ eq_proof); assumption. assumption. intros e_in_l1; exact (l1_in_l2 e e_in_l1). intro l1_not_in_l2; right; intro l1_in_l2; apply l1_not_in_l2. intros e e_in_l1; exact (l1_in_l2 e (or_intror _ e_in_l1)). intro a1_not_in_l2; right; intro l1_in_l2; apply a1_not_in_l2. apply (l1_in_l2 a1); left; reflexivity. Defined.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)