proposition: Lemma sumList_bool : forall (ls : list bool) f, NoDup ls -> (forall b, In b ls \/ (f b == 0)) -> sumList ls f == f false + f true.
proof: Proof. intuition. destruct ls. unfold sumList. simpl. rewrite ratAdd_0_r. eapply ratAdd_eqRat_compat. specialize (H0 false). simpl in H0. intuition. specialize (H0 true). simpl in H0. intuition. inversion H; clear H; subst. destruct b; rewrite sumList_cons. rewrite ratAdd_comm. eapply ratAdd_eqRat_compat; intuition. destruct ls. unfold sumList. simpl. specialize (H0 false); intuition. simpl in H3, H; intuition. discriminate. inversion H4; clear H4; subst. destruct b. simpl in H3. intuition. rewrite sumList_cons. destruct ls. unfold sumList; simpl. rewrite <- ratAdd_0_r. intuition. destruct b; simpl in *; intuition. eapply ratAdd_eqRat_compat. intuition. destruct ls. unfold sumList. simpl. specialize (H0 true). simpl in *. intuition. discriminate. inversion H4; clear H4; subst. destruct b. rewrite sumList_cons. destruct ls. unfold sumList. simpl. rewrite <- ratAdd_0_r. intuition. destruct b; simpl in *; intuition. simpl in *; intuition. Qed.
imports: Crypto FCF RndNat