proposition: Lemma eq_set_list_permut_support : forall s1 s2, eq_set s1 s2 -> LP.list_permut s1.(support) s2.(support).
proof: Proof. intros [l1 wr1]; induction l1 as [ | e1 l1]. intros [[ | e2 l2] wr2]. intros _; simpl; apply LP.list_permut_refl. intro H; assert (H' := cardinal_eq_set H); discriminate. intros [l2 wr2] H; assert (e1_in_l2 := proj1 (H e1) (or_introl _ (refl_equal _))). generalize (split_list_app_cons eq_elt_dec _ _ e1_in_l2). simpl; destruct (split_list eq_elt_dec l2 e1) as [l2' l2'']; clear e1_in_l2. intro; subst l2; assert (wr2' := without_red_remove e1 l2' l2'' wr2). apply LP.list_permut_add_cons_inside. assert (wr1' := without_red_remove e1 nil l1 wr1); simpl in wr1'. apply (IHl1 wr1' (mk_set _ wr2')). intro e; split; [intro e_in_l1 | intro e_in_l2'_l2'']. assert (e_in_l2'_e1_l2'' := (proj1 (H e)) (or_intror _ e_in_l1)). destruct (in_app_or _ _ _ e_in_l2'_e1_l2'') as [e_in_l2' | [e_eq_e1 | e_in_l2'']]. unfold mem; simpl; apply in_or_app; left; trivial. subst e; generalize wr1; simpl; destruct (eq_elt_dec e1 e1) as [ _ | e1_diff_e1]; [idtac | absurd (e1 = e1); trivial]. destruct (In_dec eq_elt_dec e1 l1) as [ _ | e1_not_in_l1]. contradiction. absurd (In e1 l1); trivial. unfold mem; simpl; apply in_or_app; right; trivial. assert (e_in_l2'_e1_l2'' : In e (l2' ++ e1 :: l2'')). destruct (in_app_or _ _ _ e_in_l2'_l2'') as [e_in_l2' | e_in_l2'']. apply in_or_app; left; trivial. apply in_or_app; right; right; trivial. generalize ((proj2 (H e)) e_in_l2'_e1_l2''); intros [e_eq_e1 | e_in_l1]; [idtac | trivial]. assert False. subst; unfold mem in e_in_l2'_l2''; simpl in e_in_l2'_l2''. clear e_in_l2'_e1_l2'' H wr1 wr2' wr1' IHl1 l1; generalize l2'' wr2 e_in_l2'_l2''; clear l2'' wr2 e_in_l2'_l2''; induction l2' as [ | e2 l2']. simpl; intro l2''; destruct (In_dec eq_elt_dec e l2'') as [e_in_l2'' | e_not_in_l2'']; trivial; intros; absurd (In e l2''); subst; trivial. intros l2'' wr2 e_in_e2_l2'_l2''; destruct (in_app_or _ _ _ e_in_e2_l2'_l2'') as [[e_eq_e2 | e_in_l2'] | e_in_l2'']. subst; generalize wr2; simpl; destruct (In_dec eq_elt_dec e (l2' ++ e :: l2'')) as [ _ | e_not_in_l2'_e_l2'']; trivial. absurd (In e (l2' ++ e :: l2'')); trivial; apply in_or_app; right; left; trivial. apply (IHl2' l2''). apply (without_red_remove e2 nil (l2' ++ e :: l2'') wr2). apply in_or_app; left; trivial. apply (IHl2' l2''). apply (without_red_remove e2 nil (l2' ++ e :: l2'') wr2). apply in_or_app; right; trivial. contradiction. Qed.
imports: List more_list list_permut Arith