proposition: Theorem shiftOut_app : forall (n : nat)(s1 s1' s2 : Blist) v, shiftOut s1 n = Some (v, s1') -> shiftOut (s1 ++ s2) n = Some (v, s1' ++ s2).
proof: Proof. induction n; simpl in *; intuition. destruct s1; simpl in *. inversion H; clear H; subst. destruct s2; simpl. trivial. trivial. inversion H; clear H; subst. rewrite app_comm_cons. trivial. destruct s1; simpl in *. discriminate. case_eq (shiftOut s1 n); intuition. rewrite H0 in H. destruct p. inversion H; clear H; subst. erewrite IHn; eauto. rewrite H0 in H. discriminate. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith