proposition: Lemma CorrectAlignedEncoderForFormatOption {S} (Some_format : FormatM S _) (None_format : FormatM () _) (encode_Some : forall sz : nat, @AlignedEncodeM _ S sz) (encode_None : forall sz : nat, @AlignedEncodeM _ () sz) (encode_Some_OK : CorrectAlignedEncoder Some_format encode_Some) (encode_None_OK : CorrectAlignedEncoder None_format encode_None) : CorrectAlignedEncoder (Option.format_option Some_format None_format) (aligned_option_encode encode_Some encode_None).
proof: Proof. exists (Option.option_encode (projT1 encode_Some_OK) (projT1 encode_None_OK)); simpl; intuition. - destruct s; simpl in *. eapply (proj1 (projT2 encode_Some_OK) s); eauto. eapply (proj1 (projT2 encode_None_OK)); eauto. - destruct s; simpl in *. eapply (proj1 (projT2 encode_Some_OK) s); eauto. eapply (proj1 (projT2 encode_None_OK)); eauto. - destruct s; simpl in *. eapply (proj1 (proj2 (projT2 encode_Some_OK))); eauto. eapply (proj1 (proj2 (projT2 encode_None_OK))); eauto. - intros ? ?. destruct s. eapply (proj2 (proj2 (projT2 encode_Some_OK)) _ s); eauto. eapply (proj2 (proj2 (projT2 encode_None_OK)) _ ()); eauto. 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