proposition: Lemma uint_of_char_spec c d d' : uint_of_char c (Some d) = Some d' -> (c = "0" /\ d' = D0 d \/ c = "1" /\ d' = D1 d \/ c = "2" /\ d' = D2 d \/ c = "3" /\ d' = D3 d \/ c = "4" /\ d' = D4 d \/ c = "5" /\ d' = D5 d \/ c = "6" /\ d' = D6 d \/ c = "7" /\ d' = D7 d \/ c = "8" /\ d' = D8 d \/ c = "9" /\ d' = D9 d \/ c = "a" /\ d' = Da d \/ c = "b" /\ d' = Db d \/ c = "c" /\ d' = Dc d \/ c = "d" /\ d' = Dd d \/ c = "e" /\ d' = De d \/ c = "f" /\ d' = Df d)%char.
proof: Proof. destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]]; intros [= <-]; intuition. Qed.
imports: Hexadecimal Ascii String