Part 1:
Until now, it was not possible, given a fact stating $\forall x. f(x) = g(x)$ to make the substitution (for example)
$\exists y. P(f(y)) \to \exists y. P(g(y))$
Without destroying and rebuilding the formula entirely. This is against the goal of the substitution steps. Now, such a substitution is possible.
Formally, it is now possible to substitute predicate and function symbols, given a proof that they are (extensionally) equal.
The PR includes tests and update to the manual.
Part 2:
The of keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of ffree schematic symbols. Manual and tests have been updated accordingly
Part 1: Until now, it was not possible, given a fact stating $\forall x. f(x) = g(x)$ to make the substitution (for example) $\exists y. P(f(y)) \to \exists y. P(g(y))$ Without destroying and rebuilding the formula entirely. This is against the goal of the substitution steps. Now, such a substitution is possible. Formally, it is now possible to substitute predicate and function symbols, given a proof that they are (extensionally) equal.
The PR includes tests and update to the manual.
Part 2: The of keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of ffree schematic symbols. Manual and tests have been updated accordingly