proposition: Lemma eq_rect_WS : forall b sz sz' w e e', eq_rect (S sz) _ (WS b w) (S sz') e = WS b (eq_rect sz _ w sz' e').
proof: Proof. simpl; intros. revert e w. rewrite e'; intro; pattern e. apply K_dec_set; eauto; decide equality. 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