> What they call a "trigger" is apparently a theorem proved by some more powerful system. (Or just assumed as an axiom. That's cheating, and it will come back to bite you.)

A trigger in SMT lingo is nothing of the sort. It’s simply an instruction to the solver about which instantiations of a universal quantifier should be considered, with the aim of getting a proof without too many specious steps.

The statement with the trigger on it is typically an assumption from e.g. a function specification. At some point the statement with the trigger may itself become a proof obligation elsewhere in the program, but that’s something that can be handled with SMT.