fact: Fixpoint getAllBlists_app(n : nat) : list Blist := match n with | 0 => nil :: nil | S n' => (map (fun ls => ls ++ (true :: nil)) (getAllBlists_app n')) ++ (map (fun ls => ls ++ (false :: nil)) (getAllBlists_app n')) end.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith