proposition: Theorem shiftOut_S_None : forall (n : nat)(s s1 : Blist)(v1 : Bvector 1), shiftOut s 1 = Some (v1, s1) -> shiftOut s1 n = None -> shiftOut s (S n) = None.
proof: Proof. Abort. Theorem shiftOut_1_None : forall (n1 n2 : nat)(s : Blist), shiftOut s n1 = None -> n2 >= n1 -> shiftOut s n2 = None. Abort. Theorem shiftOut_S : forall (n : nat)(s s1 s2 : Blist)(v1 : Bvector 1)(v2 : Bvector n), shiftOut s 1 = Some (v1, s1) -> shiftOut s1 n = Some (v2, s2) -> shiftOut s (S n) = Some (Vector.cons _ (Vector.hd v1) _ v2, s2). destruct n; intuition; simpl in *. eapply eq_trans. eapply H. specialize (shiftOut_0 s1); intuition. rewrite H0 in H1. inversion H1; clear H1; subst. f_equal. f_equal. eapply vector_hd_cons_eq. destruct s; intuition; simpl in *. discriminate. rewrite shiftOut_0 in H. inversion H; clear H; subst. rewrite H0. f_equal. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith