proposition: Lemma split2'_eq : forall sz sz' w, split2' sz sz' w = split1 sz' sz (eq_rect _ _ w _ (trans_plus_comm _ _)).
proof: Proof. induction sz; simpl; intros. - induction sz'; simpl. + shatter_word w; reflexivity. + destruct (shatter_word_S w) as (?, (w', H)); rewrite H in *; clear H. rewrite whd_eq_rect_comm; simpl. erewrite wtl_eq_rect_comm. rewrite (IHsz' w') at 1; reflexivity. - intros; destruct (shatter_word_S w) as (?, (w', H)); rewrite H in *; clear H. simpl; rewrite IHsz; clear. generalize (eq_ind_r (fun n : nat => S n = sz' + S sz) (trans_S_comm sz' sz) (trans_plus_comm sz sz')). generalize (trans_plus_comm sz sz'). fold (plus sz sz'). revert x sz w'; induction sz'; simpl; eauto. intros. assert (sz + S sz' = sz' + S sz) by omega. rewrite eq_rect_WS with (e' := H); simpl. revert w' e0 H; rewrite e; intros. destruct (shatter_word_S w') as (?, (w'', H')); rewrite H' in *; clear H'; simpl. f_equal. assert (S (sz + sz') = sz' + S sz) by omega. replace (eq_rect (S (sz' + sz)) word (WS x0 w'') (sz' + S sz) H) with (eq_rect (S (sz + sz')) word (WS x0 (eq_rect _ _ w'' _ (trans_plus_comm _ _))) (sz' + S sz) H0) by (revert w'' H H0; clear; rewrite (trans_plus_comm sz' sz); intros; simpl; destruct H; simpl; erewrite eq_rect_WS with (e' := eq_refl _); reflexivity). rewrite <- IHsz' with (e := trans_plus_comm _ _); f_equal; simpl. eapply eq_rect_split_tl. 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