always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated

normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages

function tutorial: do not omit termination proof, even when discussing other things

added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization

document new "try"

tuned comments