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