proposition: Lemma index_app : forall s s' t, index 0 (String t EmptyString) s = None -> index 0 (String t EmptyString) s' = None -> index 0 (String t EmptyString) (s ++ s')%string = None.
proof: Proof. induction s; simpl; eauto; intros. destruct (ascii_dec t a); subst. destruct s; simpl in H; try discriminate. destruct (index 0 (String t ""%string) s) eqn: ?; try discriminate. rewrite IHs; eauto. 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