proposition: Lemma index_correct' : forall s a n, index 0 (String a EmptyString) s = Some n -> exists s' s'', (s = s' ++ (String a EmptyString) ++ s'' /\ String.length s' = n)%string /\ index 0 (String a EmptyString) s' = None.
proof: Proof. induction s; simpl; intros; try discriminate. destruct (ascii_dec a0 a). - destruct s; simpl in H; injections. eexists ""%string, ""%string; split; eauto. eexists ""%string, _; split; simpl; eauto. - destruct (index 0 (String a0 EmptyString) s) eqn: ?; injections; try discriminate. apply IHs in Heqo; destruct_ex; intuition; subst. eexists (String a _), _; simpl; split; eauto. destruct (ascii_dec a0 a); try congruence. rewrite H1; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Computation.Core Fiat.Computation.FixComp Fiat.Computation.Notations Fiat.Computation.Refinements.General Fiat.Common.DecideableEnsembles Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.AsciiOpt