remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations

avoid double ASCII-fication

make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity

generate type predicates for existentials/skolems, otherwise some problems might not be provable

insert rather than append special facts to make it less likely that they're truncated away

hidden font: full height makes cursor more visible;