// e.g. in = "very $x", out = "$x"
svoid philosophyBot1_addSimplificationRule_withTrails(PhilosophyBot1 bot, S ruleIn, S ruleOut, S originalFact) {
  Set<T3S> replacements = cast bot.getExtension("simplification rules");
  if (replacements == null) {
    // first time, register extension and set up transformer
    bot.addExtension("simplification rules", replacements = new Set);
    Set<T3S> _replacements = replacements;
    bot.addTrailEnabledDeepTransformer(s -> {
      for (T3S p : _replacements) {
        S out = simpleRewriteWithDollarVars(p.a, p.b, s);
        if (out != null)
          ret WithTrail(litorderedmap(op := "simplification rule",
            +p, +s, +out, originalFact := p.c), out);
      }
      null;
    });
  }
  // after that, just add new replacement pair to the list
  replacements.add(t3(ruleIn, ruleOut, originalFact));
}