proposition: Lemma split_char_inj : forall s s' t t', (s ++ String "." s' = t ++ String "." t')%string -> index 0 "." s = None -> index 0 "." t = None -> s = t /\ s' = t'.
proof: Proof. induction s. - destruct t. + simpl; intros; injections; intuition eauto. + intros; simpl in H; injection H; intros; subst. simpl in H1. destruct t; simpl in H1; discriminate. - intros; destruct t. + simpl in H; injection H; intros; subst. simpl in H0; destruct s; simpl in H0; discriminate. + simpl in H; injection H; intros; subst. simpl in *; repeat find_if_inside; try discriminate. destruct (index 0 "." s) eqn: ?; destruct (index 0 "." t) eqn : ?; try discriminate. apply IHs in H2; eauto. intuition. congruence. 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