// Fig. 4.10
// The taclet described in Example 4.35
// (the taclet given here already exists as base rule in KeY)

\sorts {
  \generic G;
}
\schemaVariables {
  \formula phi;      \variables G x;      \term G s;
}
\rules {
  instAll { \assumes (\forall x; phi ==>) \find (s)
            \add ({\subst x; s}phi ==>) };
}