proposition: Theorem shiftOut_plus : forall (n1 n2 : nat) s b s', shiftOut s (n1 + n2) = Some (b, s') -> exists b1 b2 s'', shiftOut s n1 = Some (b1, s'') /\ shiftOut s'' n2 = Some (b2, s') /\ splitVector n1 n2 b = (b1, b2).
proof: Proof. induction n1; intuition; simpl in *. rewrite shiftOut_0. econstructor. econstructor. econstructor. intuition. trivial. destruct s; simpl in *. discriminate. case_eq (shiftOut s (n1 + n2)); intuition. rewrite H0 in H. destruct p. inversion H; clear H; subst. edestruct IHn1. eauto. destruct H. destruct H. intuition. rewrite H1. econstructor. econstructor. econstructor. intuition. eauto. simpl. rewrite H3. trivial. rewrite H0 in H. discriminate. Qed.
imports: FCF.FCF FCF.SemEquiv FCF.DetSem