proposition: Lemma getUnusedR_eq : forall ls1 ls2 x, (forall r, inRange ls1 r = inRange ls2 r) -> evalDist (getUnusedR ls1) x == evalDist (getUnusedR ls2) x.
proof: Proof. intuition. destruct (in_dec (EqDec_dec _) x (getSupport (getUnusedR ls1))). unfold getUnusedR in *. simpl in i. apply filter_In in i; intuition. eapply evalDist_Repeat_eq. intuition. rewrite H. trivial. eapply filter_In; intuition. eapply sumList_permutation. eapply NoDup_Permutation. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_NoDup. eapply getSupport_NoDup. intuition. apply filter_In in H2; intuition. eapply filter_In; intuition. rewrite <- H. trivial. apply filter_In in H2; intuition. eapply filter_In; intuition. rewrite H. trivial. unfold getUnusedR in *. simpl in n. apply filter_not_In in n. intuition. simpl. rewrite getSupport_not_In_evalDist_h; intuition. repeat rewrite ratMult_0_r. intuition. simpl. unfold indicator. rewrite <- H. rewrite H0. repeat rewrite ratMult_0_l. intuition. Qed.
imports: Crypto Permutation CompFold Array FCF State