proposition: Lemma terminal_char_eq : forall x0, terminal_char = ascii_of_N (wordToN x0) -> x0 = wzero 8.
proof: Proof. intros. unfold terminal_char, zero in H. shatter_word x0. simpl in H. repeat (find_if_inside; simpl in H); try discriminate. 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