CHAR_EQ_CONV : term -> thm
|- s = t <=> T or |- s = t <=> F
# let t = mk_eq(mk_char 'A',mk_char 'A');; val t : term = `ASCII F T F F F F F T = ASCII F T F F F F F T` # CHAR_EQ_CONV t;; val it : thm = |- ASCII F T F F F F F T = ASCII F T F F F F F T <=> T