renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"

merged

avoid duplicate facts, which confuse the minimizer output

pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types

restore comment about subtle issue

made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded

don't launch the automatic minimizer for zero facts

don't generate unsound proof error for missing proofs

renamed option to avoid talking about seconds, since this is now the default Isabelle unit

fixed format selection logic for Waldmeister