proposition: Lemma getAllBlists_app_NoDup : forall n, NoDup (getAllBlists_app n).
proof: Proof. induction n; intuition; simpl in *. econstructor. simpl. intuition. econstructor. eapply app_NoDup; intuition. eapply map_NoDup; intuition. eapply H. apply app_inj_tail in H0. intuition. eapply map_NoDup; intuition. eapply H. eapply app_inj_tail in H0. intuition. apply in_map_iff in H. apply in_map_iff in H0. destruct H. destruct H0. intuition. subst. apply app_inj_tail in H; intuition. apply in_map_iff in H. apply in_map_iff in H0. destruct H. destruct H0. intuition. subst. apply app_inj_tail in H; intuition. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation