proposition: Lemma getAllBvectors_NoDup : forall (n : nat), NoDup (getAllBvectors n).
proof: Proof. induction n; intuition; simpl in *. econstructor. eapply in_nil. econstructor. eapply app_NoDup. eapply map_NoDup; eauto. intros. eapply vector_cons_ne; eauto. eapply map_NoDup; eauto. intros. eapply vector_cons_ne; eauto. intuition. apply in_map_iff in H. apply in_map_iff in H0. destruct H. destruct H0. intuition. subst. inversion H. intuition. apply in_map_iff in H. apply in_map_iff in H0. destruct H. destruct H0. intuition. subst. inversion H. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith