proposition: Lemma align_decode_sumtype_OK' {m : nat} {types : t Type m} (align_decoders : ilist (B := fun T => forall n, ByteBuffer.t n -> CacheDecode -> option (T * {n : _ & ByteBuffer.t n} * CacheDecode)) types) (decoders : ilist (B := fun T => ByteString -> CacheDecode -> option (T * ByteString * CacheDecode)) types) (decoders_OK : forall n v cd idx', ith decoders idx' (build_aligned_ByteString v) cd = Ifopt ith align_decoders idx' n v cd as a Then Some (fst (fst a), build_aligned_ByteString (projT2 (snd (fst a))), snd a) Else None) : forall (idx : Fin.t m) {n : nat} (v : ByteBuffer.t n) (cd : CacheDecode), decode_SumType types decoders idx (build_aligned_ByteString v) cd = Ifopt align_decode_sumtype align_decoders idx v cd as a Then Some (fst (fst a), build_aligned_ByteString (projT2 (snd (fst a))), snd a) Else None.
proof: Proof. intros. unfold decode_SumType, align_decode_sumtype. rewrite decoders_OK. destruct (ith align_decoders idx n v cd) as [ [ [? ?] ?] | ]; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt 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.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word