proposition: Lemma enqueue_opt_format_word : forall n w b b', enqueue_opt b (encode_word' n w b') = mappend (encode_word' n w b') (enqueue_opt b mempty).
proof: Proof. induction w; simpl; intros; eauto. - rewrite <- enqueue_mappend_opt, mempty_right; auto. - rewrite !IHw. rewrite <- mappend_assoc. rewrite <- !enqueue_mappend_opt, !mempty_right. rewrite IHw; 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