proposition: Theorem rndListElem_uniform : forall (A : Set)(eqd : EqDec A)(ls : list A)(a1 a2 : option A), NoDup ls -> In a1 (getSupport (rndListElem _ ls)) -> In a2 (getSupport (rndListElem _ ls)) -> evalDist (rndListElem _ ls) a1 == evalDist (rndListElem _ ls) a2.
proof: Proof. intuition. destruct a1. destruct a2. rewrite <- rndListElem_support in *. unfold rndListElem. case_eq (length ls); intuition. destruct ls; simpl in *. intuition. lia. eapply comp_spec_impl_eq. eapply comp_spec_seq. apply (Some a). apply (Some a). eapply eq_impl_comp_spec. eapply well_formed_RndNat. lia. eapply well_formed_RndNat. lia. eapply RndNat_uniform. 3:{ intros. simpl in H5. eapply comp_spec_ret. assert (a1 = (firstIndexOf (EqDec_dec _) ls a 0) <-> b = (firstIndexOf (EqDec_dec _) ls a0 0)). eapply H5. clear H5. intuition; subst. rewrite H5. eapply nth_firstIndexOf; trivial. symmetry. eapply nth_firstIndexOf_if; intuition. rewrite H7. eapply nth_firstIndexOf; trivial. symmetry. eapply nth_firstIndexOf_if; intuition. } rewrite <- H2. apply firstIndexOf_in_lt; trivial. rewrite <- H2. apply firstIndexOf_in_lt; trivial. apply rndListElem_support in H0. apply rndListElem_support_None in H1. subst. simpl in *. intuition. destruct a2. apply rndListElem_support in H1. apply rndListElem_support_None in H0. subst. simpl in *. intuition. intuition. Qed.
imports: FCF.FCF