General substitution utilities
Adding an extension to the general Substitution
tactic to allow full sequent simultaneous formula/term substitutions
Works now.
Substitutions can be performed in the following manner now:
have(P(x) |- P(x) \/ Q(y)) by Restate
thenHave((P(x), x === y) |- P(y) \/ R(x)) by Substitution(QyIffRx, x === y)
where QyIffRx
is a theorem Q(y) <=> R(y)
in its RHS (and in this case, only () |- Q(y) <=> R(x)
)