proposition: Lemma align_format_sumtype_OK' {m : nat} {types : t Type m} (align_encoders_n : ilist2.ilist2 (B := fun T : Type => T -> CacheFormat -> nat) types) (align_encoders_v : i2list (B := fun T : Type => T -> CacheFormat -> nat) (fun (T : Type) (n : _) => forall t ce, Vector.t (word 8) (n t ce)) align_encoders_n) (align_encoders_ce : ilist (B := (fun T : Type => T -> CacheFormat -> CacheFormat)) types) (formatrs : ilist (B := (fun T : Type => T -> @CacheFormat cache -> Comp (ByteString * (CacheFormat)))) types) (formatrs_OK : forall idx t (ce : CacheFormat), refine (ith formatrs idx t ce) (ret (build_aligned_ByteString (i2th align_encoders_v idx t ce), ith align_encoders_ce idx t ce))) : forall (st : SumType types) (ce : CacheFormat), refine (format_SumType types formatrs st ce) (ret (build_aligned_ByteString (projT2 (fst (align_format_sumtype align_encoders_n align_encoders_v align_encoders_ce st ce))), (snd (align_format_sumtype align_encoders_n align_encoders_v align_encoders_ce st ce)))).
proof: Proof. intros; unfold format_SumType, align_format_sumtype. rewrite formatrs_OK; reflexivity. Qed.
imports: Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.i2list Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecoders Bedrock.Word