proposition: Lemma getAllBlists_In_length : forall n ls, In ls (getAllBlists n) -> length ls = n.
proof: Proof. induction n; intuition; simpl in *. destruct H; subst; intuition. apply in_app_or in H; destruct H; apply in_map_iff in H; destruct H; intuition; subst; simpl; f_equal; eapply IHn; eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation