proposition: Lemma shiftOut_ls_eq : forall n ls1 ls2 v ls1' ls2', shiftOut ls1 n = Some (v, ls1') -> shiftOut ls2 n = Some (v, ls2') -> (firstn n ls1) = (firstn n ls2).
proof: Proof. induction n; intuition; simpl in *. destruct ls1; simpl in *; try discriminate. destruct ls2; simpl in *; try discriminate. case_eq (shiftOut ls1 n); intuition. rewrite H1 in H. case_eq (shiftOut ls2 n); intuition. rewrite H2 in H0. destruct p. destruct p0. inversion H; clear H; subst. apply opt_eq_inv in H0. apply pair_eq_inv in H0; intuition. apply vector_cons_eq_inv in H; intuition; subst. f_equal. eapply IHn. eapply H1. eapply H2. rewrite H2 in H0. discriminate. rewrite H1 in H. discriminate. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation