proposition: Lemma AlignedFormatSumTypeDoneC {m : nat} {types : t Type m} (A_OKs_l : ilist (B := fun T : Type => T -> Prop) types) (A_OKs : SumType types -> Prop := fun st => ith A_OKs_l (SumType_index _ st) (SumType_proj _ st)) (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) (encoders : ilist (B := (fun T : Type => T -> CacheFormat -> Comp (ByteString * (CacheFormat)))) types) (encoders_OK : Iterate_Ensemble_BoundedIndex (fun idx => forall t (ce : CacheFormat), A_OKs (inj_SumType _ idx t) -> refine (ith encoders 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), A_OKs st -> refine (((format_SumType types encoders st) DoneC) 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. etransitivity. eapply AlignedFormatDoneC. rewrite (align_format_sumtype_OK_inv A_OKs); try eassumption. instantiate (2 := fun ce => fst (align_format_sumtype align_encoders_n align_encoders_v align_encoders_ce st ce)). instantiate (1 := fun ce => snd (align_format_sumtype align_encoders_n align_encoders_v align_encoders_ce st ce)). simpl; reflexivity. simpl; 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