proposition: Lemma eq_set_list_permut_support : forall s1 s2, eq_set s1 s2 -> permut s1.(support) s2.(support).
proof: Proof. intros [l1 wr1] [l2 wr2]; unfold eq_set, mem; simpl; revert l2 wr2; induction l1 as [ | e1 l1]. intros [ | e2 l2] _ H. apply Pnil. apply False_rect. generalize (H e2); simpl; intros [_ Abs]; apply Abs; left; reflexivity. intros l2 wr2 H. assert (e1_in_l2 : more_list.mem eq_A e1 l2). rewrite <- H; left; reflexivity; trivial. destruct (mem_split_set _ _ eq_bool_ok _ _ e1_in_l2) as [e1' [l2' [l2'' [e1_eq_e1' [H' _]]]]]. simpl in e1_eq_e1'; simpl in H'; subst l2. rewrite <- permut_cons_inside; trivial. apply IHl1; trivial. apply (without_red_remove e1 nil); trivial. apply (without_red_remove e1'); trivial. intros e; split; intro H'. apply diff_mem_remove with e1'. intro e_eq_e1'; apply (without_red_not_in e1 nil l1 wr1). simpl; rewrite e1_eq_e1'; rewrite <- e_eq_e1'; trivial. rewrite <- (H e); right; trivial. apply (@diff_mem_remove _ eq_A nil l1 e1). intro e_eq_e1; apply (without_red_not_in e1' l2' l2'' wr2). rewrite <- e1_eq_e1'; rewrite <- e_eq_e1; trivial. rewrite (H e); apply mem_insert; trivial. Qed.
imports: Coq(Relations List Setoid Arith FunInd) CoLoR(decidable_set more_list list_permut)