proposition: Lemma wtl_eq_rect_S : forall sz sz' w eq_comm eq_comm', wtl (eq_rect (S sz) word w (S sz') eq_comm) = eq_rect sz word (wtl w) sz' eq_comm'.
proof: Proof. intros. destruct (shatter_word_S w) as (?, (w', H)); rewrite H in *; clear. revert w' eq_comm. rewrite eq_comm'; clear eq_comm'; intros. unfold eq_rect; simpl. revert w'. pattern eq_comm. 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