Use `byte` based strings for proof mode

Newer versions of Coq have a type byte with 256 constructors. We could use strings based on byte in the proofmode. Maybe that gives a significant speed up compared to the current ascii based strings.

@tchajed said the construction of byte based strings does not exist in the Coq stdlib but can be defined as:

From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.

Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.

Definition foo : bytes := "foo".