im.bldsbt

Theorem.

Arguments:

y (st), x (sv), phi (pr), psi (pr),

Assertions:

(forallx(phitopsi)to([y/x]phito[y/x]psi))

Proof:

Hyp Ref Line Expr
spec1(forallx(phitopsi)to[y/x](phitopsi))
sb-im2([y/x](phitopsi)leftrightarrow([y/x]phito[y/x]psi))
1, 2brpi223(forallx(phitopsi)to([y/x]phito[y/x]psi))