proposition: Lemma sumList_rel_ls_intersect: forall (A : Set)(rel : A -> Rat -> Prop)(ls1 : list A) r, sumList_rel rel ls1 r -> forall ls2, NoDup ls1 -> NoDup ls2 -> eq_dec A -> (forall a r1 r2, In a ls1 -> rel a r1 -> rel a r2 -> r1 == r2) -> (forall a, In a ls1 -> ~In a ls2 -> rel a 0) -> (forall a, In a ls2 -> ~In a ls1 -> rel a 0) -> sumList_rel rel ls2 r.
proof: Proof. induction 1; intuition; simpl in *. eapply sumList_rel_body_eq. eapply sumList_rel_all_0. intuition. eapply H5. eauto. simpl. intuition. intuition. intuition. trivial. inversion H2; clear H2; subst. symmetry in H1. eapply sumList_rel_body_eq; intuition; eauto. clear H1. clear r3. destruct (in_dec H4 a ls2). eapply sumList_rel_permutation. eapply Permutation_sym. eapply removeFirst_permutation. eauto. econstructor. eapply IHsumList_rel; intuition. eapply removeFirst_NoDup. trivial. eapply H5. right. eapply H1. trivial. trivial. eapply H6. intuition. intuition. eapply H2. eapply removeFirst_in. trivial. intuition. subst. intuition. destruct (H4 a a0); subst. eapply H6. intuition. intuition. eapply removeFirst_NoDup_not_in. eapply H3. eauto. eapply H7. eapply removeFirst_in_iff. eauto. simpl. intuition. eauto. intuition. assert (rel a 0). eapply H6. intuition. intuition. assert (r2 == 0). eapply H5. eauto. trivial. trivial. eapply sumList_rel_body_eq. 3:{ rewrite H2. rewrite <- ratAdd_0_l. eapply eqRat_refl. } 2:{ intuition. eauto. } 2:{ eauto. } eapply IHsumList_rel; intuition. eapply H5. right. eauto. trivial. trivial. eapply H7. trivial. intuition. subst. intuition. Unshelve. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation