proposition: Lemma SetCurrentBytes_SetCurrentBytes' : forall n sz v idx w c, @SetCurrentBytes n sz v idx w c = @SetCurrentBytes' n sz v idx w c.
proof: Proof. induction sz; simpl; intros. - reflexivity. - destruct sz; unfold AppendAlignedEncodeM, SetCurrentByte; destruct (_ <? _) eqn:?; unfold If_Opt_Then_Else. + unfold SetCurrentBytes', AlignedEncode_Nil, ReturnAlignedEncodeM; simpl. destruct (S _ <? S _) eqn:?; rewrite ?Nat.ltb_lt, ?Nat.ltb_ge, ?split1'_8_0 in *; (reflexivity || omega). + reflexivity. + rewrite IHsz; reflexivity. + reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad