proposition: Lemma rel_map_Rnd_any_in : forall n ls (a : Bvector n), rel_map (evalDet (Rnd n)) (getAllBlists n) ls -> In (ca_done a) ls.
proof: Proof. intuition. eapply (rel_map_in H _ _ (VectorDef.to_list a)). eapply getAllBlists_length_In. eapply to_list_length. econstructor. econstructor. eauto. simpl. rewrite shiftOut_to_list. econstructor. eauto. simpl. econstructor. Unshelve. intuition. eapply evalDet_func; eauto. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat