proposition: Lemma decode_encode_word'_Some : forall sz bin data ext, decode_word' sz bin = Some (data, ext) -> bin = mappend (encode_word' sz data mempty) ext.
proof: Proof. induction sz0; simpl; intros. - shatter_word data; simpl; injections. rewrite mempty_left; auto. - destruct (dequeue_opt bin) as [ [? ?] | ] eqn: ? ; simpl in *; try discriminate. destruct (decode_word' sz0 t) as [ [? ?] | ] eqn: ? ; simpl in *; try discriminate. injections. apply IHsz0 in Heqo0; subst. eapply dequeue_opt_inj; eauto. simpl. rewrite <- dequeue_encode_word'_enqueue_opt. clear; revert ext; induction w; simpl; auto; intros. rewrite !enqueue_opt_format_word, <- !mappend_assoc. 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