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