Update AES128.v

[rkashghari]

Added the hex Inductive type to the end of the document before the code extractions. The problem is that each hex value (1 to f) has a different constructor, so making functions around that take hex types as input and matching each constructor is a problem. The only thing I could think of when converting the 32 hex digits into a 16 byte matrix was to do an exhaustive mapping between, which would literally required 2^128 cases.