proposition: Theorem rndListElem_uniform_gen : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(ls1 : list A)(ls2 : list B)(a1 : A)(a2 : B), NoDup ls1 -> NoDup ls2 -> length ls1 = length ls2 -> In a1 ls1 -> In a2 ls2 -> comp_spec (fun x y => x = Some a1 <-> y = Some a2) (rndListElem _ ls1) (rndListElem _ ls2).
proof: Proof. intuition. unfold rndListElem. case_eq (length ls1); intuition. rewrite <- H1. rewrite H4. eapply comp_spec_ret; intuition. discriminate. discriminate. rewrite <- H1. rewrite H4. eapply comp_spec_seq; try eapply None. eapply eq_impl_comp_spec. eapply well_formed_RndNat; lia. eapply well_formed_RndNat; lia. eapply (@RndNat_uniform (firstIndexOf (EqDec_dec _) ls1 a1 O) (firstIndexOf (EqDec_dec _) ls2 a2 O)). rewrite <- H4. apply firstIndexOf_in_lt; trivial. rewrite <- H4. rewrite H1. apply firstIndexOf_in_lt; trivial. intuition. eapply comp_spec_ret. intuition. destruct (eq_nat_dec a (firstIndexOf (EqDec_dec _) ls1 a1 O)). subst. assert (b = firstIndexOf (EqDec_dec _) ls2 a2 0); intuition. subst. repeat rewrite nth_firstIndexOf; intuition. assert (b <> firstIndexOf (EqDec_dec _) ls2 a2 0). intuition. exfalso. eapply nth_firstIndexOf_None. eapply H. eapply H2. eapply n0. eauto. intuition. destruct (eq_nat_dec a (firstIndexOf (EqDec_dec _) ls1 a1 O)). subst. assert (b = firstIndexOf (EqDec_dec _) ls2 a2 0); intuition. subst. repeat rewrite nth_firstIndexOf; intuition. assert (b <> firstIndexOf (EqDec_dec _) ls2 a2 0). intuition. exfalso. eapply nth_firstIndexOf_None. eapply H0. eapply H3. eapply H10. eauto. intuition. Qed.
imports: FCF.FCF