proposition: Lemma ptr_eq : forall (p p' : {w : word 8 | wlt (natToWord 8 191) w}), proj1_sig p = proj1_sig p' -> p = p'.
proof: Proof. intros [p p_pf] [p' p'_pf]; simpl; intros; subst. f_equal. unfold wlt, BinNat.N.lt in *. apply UIP_dec. decide equality. 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