// Fig. 4.4
// Examples of taclets implementing first-order rules
// (the taclets given here already exist as base rules in KeY)

\sorts {
  \generic G;
}
\schemaVariables {
  \formula phi;            \variables G x;
  \skolemTerm G cnst;      \term G s;
}
\rules {
  allLeft   { \find (\forall x; phi ==>)
              \add ({\subst x; s}phi ==>) };
  allRight  { \find (==> \forall x; phi)
              \varcond (\new(cnst, \dependingOn(phi)))
              \replacewith (==> {\subst x; cnst}phi) };
}