fact: Fixpoint shiftOut(s : Blist)(n : nat) : option (Bvector n * Blist) := match n with | 0 => Some ((@Vector.nil bool), s) | S n' => match s with | nil => None | b :: s' => match (shiftOut s' n') with | Some (v', s'') => Some (Vector.cons _ b _ v', s'') | None => None end end end.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith