proposition: Theorem in_getAllBvectors : forall (n : nat)(v : Bvector n), In v (getAllBvectors n).
proof: Proof. induction v; intuition; simpl. auto. eapply in_or_app; intuition. destruct h. left. eapply in_map; eauto. right. eapply in_map; eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith