Closed sankalpgambhir closed 1 year ago
Adding an extension to the general Substitution tactic to allow full sequent simultaneous formula/term substitutions
Substitution
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))
QyIffRx
Q(y) <=> R(y)
() |- Q(y) <=> R(x)
Adding an extension to the general
Substitutiontactic to allow full sequent simultaneous formula/term substitutionsWorks now.
Substitutions can be performed in the following manner now:
where
QyIffRxis a theoremQ(y) <=> R(y)in its RHS (and in this case, only() |- Q(y) <=> R(x))