proposition: Lemma dequeue_opt_Some' : forall n w ext, dequeue_opt (mappend (encode_word' (S n) w mempty) ext) = Some (word_split_hd w, (mappend (encode_word' n (word_split_tl w) mempty) ext)).
proof: Proof. induction n; simpl; intros. - shatter_word w; simpl in *. erewrite dequeue_mappend_opt; eauto using dequeue_head_opt. - destruct (shatter_word_S w) as (?, (?, ?)); subst; simpl. simpl in *. rewrite enqueue_opt_format_word. rewrite <- mappend_assoc. rewrite IHn. rewrite enqueue_opt_format_word. rewrite <- mappend_assoc; auto. 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