proposition: Lemma rel_map_Rnd_NoDup : forall n ls, rel_map (evalDet (Rnd n)) (getAllBlists n) ls -> NoDup ls.
proof: Proof. intuition. eapply rel_map_NoDup. eauto. eapply getAllBlists_NoDup. intuition. subst. inversion H4; clear H4; subst. inversion H5; clear H5; subst. inversion H3; clear H3; subst. inversion H5; clear H5; subst. simpl in *. edestruct shiftOut_Some. eapply le_refl_gen. symmetry. eapply getAllBlists_In_length. eauto. rewrite H3 in H9. edestruct shiftOut_Some. eapply le_refl_gen. symmetry. eapply getAllBlists_In_length. eapply H0. rewrite H4 in H8. destruct x. destruct x0. inversion H9; clear H9; subst. inversion H8; clear H8; subst. simpl in *. inversion H11; clear H11; subst. inversion H10; clear H10; subst. eapply H2. specialize (shiftOut_ls_eq _ _ H3 H4); intuition; eauto. erewrite <- (firstn_eq_all_gen a1). erewrite <- (firstn_eq_all_gen a2). eauto. symmetry. eapply getAllBlists_In_length. trivial. symmetry. eapply getAllBlists_In_length. trivial. inversion H5; clear H5; subst. simpl in *. edestruct shiftOut_Some. eapply le_refl_gen. symmetry. eapply getAllBlists_In_length. eapply H1. rewrite H4 in H9. destruct x. inversion H9; clear H9; subst. simpl in *. inversion H10. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat