proposition: Lemma eq_rect_split_tl : forall (sz sz' : nat) (x0 : bool) (w'' : word (sz' + sz)) (e : sz' + sz = sz + sz') (e1 : sz + sz' = sz' + sz), word_split_tl (WS x0 w'') = eq_rect (sz + sz') word (word_split_tl (WS x0 (eq_rect (sz' + sz) word w'' (sz + sz') e))) (sz' + sz) e1.
proof: Proof. induction sz; simpl. - intro; rewrite <- plus_n_O; intros. pattern e1. apply K_dec_set; eauto; try decide equality; clear e1. pattern e. apply K_dec_set; eauto; try decide equality; clear e. - intro; rewrite <- (trans_S_comm sz' sz); intros. intros; destruct (shatter_word_S w'') as (?, (w', H)); rewrite H in *; clear H. simpl. rewrite (IHsz sz' x w' (trans_plus_comm _ _) (trans_plus_comm _ _)); repeat f_equal. erewrite !eq_rect_WS; 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