proposition: Theorem shiftOut_plus_if : forall n1 n2 s s' s'' b1 b2, shiftOut s n1 = Some (b1, s') -> shiftOut s' n2 = Some (b2, s'') -> shiftOut s (n1 + n2) = Some (Vector.append b1 b2, s'').
proof: Proof. induction n1; intuition; simpl in *. rewrite shiftOut_0 in H. inversion H; clear H; subst. simpl in *. trivial. destruct s; simpl in *. discriminate. case_eq (shiftOut s n1); intuition. rewrite H1 in H. destruct p. inversion H; clear H; subst. erewrite IHn1; eauto. rewrite Vector_cons_app_assoc. trivial. rewrite H1 in H. discriminate. Qed.
imports: FCF.FCF FCF.SemEquiv FCF.DetSem