fact: Definition hd d := match d with | Nil => 0x0 | D0 _ => 0x0 | D1 _ => 0x1 | D2 _ => 0x2 | D3 _ => 0x3 | D4 _ => 0x4 | D5 _ => 0x5 | D6 _ => 0x6 | D7 _ => 0x7 | D8 _ => 0x8 | D9 _ => 0x9 | Da _ => 0xa | Db _ => 0xb | Dc _ => 0xc | Dd _ => 0xd | De _ => 0xe | Df _ => 0xf end.
imports: Hexadecimal HexadecimalFacts Arith