proposition: Lemma calculate_aligned_IPchecksum_eq m {sz} (v : ByteBuffer.t sz) (idx : nat) : calculate_aligned_IPchecksum' m v idx = calculate_aligned_IPchecksum'' m v idx.
proof: Proof. unfold calculate_aligned_IPchecksum'. revert v m. revert sz. induction idx; simpl; intros; try easy. destruct v; simpl; rewrite <- Eqdep_dec.eq_rect_eq_dec; try apply Nat.eq_dec. - destruct m. reflexivity. destruct m; reflexivity. - destruct idx; eauto. assert (n = n - 0) as L by omega. replace (ByteBuffer.drop 0 v) with (eq_rect _ _ v _ L). destruct L. simpl. reflexivity. simpl. f_equal. apply Eqdep_dec.UIP_dec. apply Nat.eq_dec. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Bedrock.Word