proposition: Lemma getAllBvectors_length : forall n, length (getAllBvectors n) = (expnat 2 n).
proof: Proof. induction n; intuition; simpl in *. rewrite app_length. repeat rewrite map_length. rewrite Nat.add_0_r. f_equal; eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith