proposition: Lemma getAllBlists_app_length_In : forall n ls, length ls = n -> In ls (getAllBlists_app n).
proof: Proof. induction n; intuition; simpl in *; destruct ls; simpl in *; intuition; try lia. edestruct (ls_last_exists (b :: ls)). simpl. eauto. destruct H0. intuition. rewrite H2. eapply in_or_app. destruct x; [left | right]; eapply in_map_iff; econstructor; intuition. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation