proposition: Theorem shiftOut_plus_None : forall n1 n2 s, shiftOut s (n1 + n2) = None -> shiftOut s n1 = None \/ (exists x s', shiftOut s n1 = Some (x, s') /\ shiftOut s' n2 = None).
proof: Proof. induction n1; intuition; simpl in *. rewrite shiftOut_0. right. econstructor. econstructor. intuition. destruct s; simpl in *. intuition. case_eq (shiftOut s (n1 + n2)); intuition. rewrite H0 in H. destruct p. discriminate. edestruct IHn1. eauto. rewrite H1. intuition. destruct H1. destruct H1. intuition. rewrite H2. right. econstructor. econstructor. intuition. Qed.
imports: FCF.FCF FCF.SemEquiv FCF.DetSem