proposition: Lemma shiftOut_Some : forall (ls : Blist) n, length ls >= n -> exists p, shiftOut ls n = Some p.
proof: Proof. induction ls; intuition; simpl in *. assert (n = O). lia. subst. exists ([], nil). trivial. destruct n. exists ([], a :: ls). trivial. assert (length ls >= n). lia. destruct (IHls n). trivial. destruct x. econstructor. rewrite H1. eauto. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith