proposition: Lemma cacheAddDNPointer_pf : forall (ce : CacheFormat) (cd : CacheDecode) (t : string * pointerT), Equiv ce cd -> add_ptr_OK t ce cd -> Equiv (fst ce, association_list_add (snd ce) (fst t) (snd t)) (fst cd, association_list_add (snd cd) (snd t) (fst t)).
proof: Proof. simpl; intuition eauto; simpl in *; subst; eauto. unfold add_ptr_OK in *. destruct t; simpl in *; simpl; econstructor; eauto. clear H3; induction b0; simpl. - intuition. - simpl in H0; destruct a; find_if_inside; try discriminate. intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.DNSPacket Bedrock.Word