proposition: Lemma word_split_SW {n} : forall (w : word (S n)), w = SW_word (word_split_hd w) (word_split_tl w).
proof: Proof. induction n; simpl; intros. - shatter_word w; reflexivity. - destruct (shatter_word_S w) as (?, (?, ?)); subst; simpl. rewrite (IHn x0) at 1; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats