Skip to content

General substitution utilities

Sankalp Gambhir requested to merge github/fork/sankalpgambhir/subst-improve-1 into main

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))

Merge request reports