proposition: Lemma AlignedFormat_If_Then_Else {numBytesT numBytesE} : forall (b : bool) ctx ctxT ctxE (vT : Vector.t Core.char numBytesT) (vE : Vector.t Core.char numBytesE) (format1 format2 : CacheFormat -> Comp (_ * CacheFormat)), (b = true -> refine (format1 ctx) (ret (build_aligned_ByteString vT, ctxT))) -> (b = false -> refine (format2 ctx) (ret (build_aligned_ByteString vE, ctxE))) -> refine (If b Then (format1 ctx) Else (format2 ctx)) (ret (build_aligned_ByteString (Variational_Vector b vT vE) , If b Then ctxT Else ctxE)).
proof: Proof. destruct b; simpl; intros; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.Ascii Coq.Strings.String Coq.Numbers.BinNums Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Bedrock.Word Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Automation.Solver Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders