proposition: Lemma ByteString_mempty_right : forall bs : ByteString, ByteString_append bs ByteString_id = bs.
proof: Proof. destruct bs; unfold ByteString_append, ByteString_id; simpl. rewrite ByteString_push_char_id_right; simpl; eauto. rewrite app_nil_r. induction front0. + simpl; f_equal. pose ByteString_id_subproof. eapply le_uniqueness_proof. + simpl. assert (lt n 8) by (unfold lt; omega). erewrite (IHfront0 H). unfold ByteString_push. simpl. destruct (eq_nat_dec n 7); subst. omega. f_equal; eauto using le_uniqueness_proof. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs