(8steps total)
PrintForm
Definitions
Lemmas
ElisTarskiPf
A
Sections
NuprlLIB
Doc
At:
s2
1
1
2
1.
t:
Term
SUBX(
f(t); UP(
f(t)))
= SUBX(f(t);
f(t))
By:
BackThru
Thm*
t,r,t',r':Term. t
= t' & r
= r'
SUBX(t; r)
= SUBX(t'; r')
Generated subgoal:
1
f(t)
= f(t) & UP(
f(t))
=
f(t)
3
steps
About:
(8steps total)
PrintForm
Definitions
Lemmas
ElisTarskiPf
A
Sections
NuprlLIB
Doc
f(t) 
= f(t) & UP(f(t)) = f(t)
SUBX(f(t); UP(f(t))) = SUBX(f(t); f(t))
t,r,t',r':Term. t = t' & r = r' 
SUBX(t; r) = SUBX(t'; r')
f(t) = f(t) & UP(f(t)) = f(t)
