proposition: Lemma pointerT_eq_dec : forall p p' : pointerT, {p = p'} + {p <> p'}.
proof: Proof. intros. rewrite <- (Nat2pointerT_pointerT2Nat p), <- (Nat2pointerT_pointerT2Nat p'). destruct (Peano_dec.eq_nat_dec (pointerT2Nat p) (pointerT2Nat p')). left; rewrite e; congruence. right; intro; apply n. rewrite !Nat2pointerT_pointerT2Nat in H; 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