(7steps total) PrintForm Lemmas ElisTarskiPf A Sections NuprlLIB Doc

At: qsubx repst 1 1 1 1
1. t: Term
2. r: Term
3. t': Term
4. r': Term
5. t Term
6. t = t'
7. r Term
8. r = r'
SUBX(t; r) Term
By: BackThru Thm* t,r:Term. t Term & r Term SUBX(t; r) Term
Generated subgoals:

None

About:
equalimpliesandall

(7steps total) PrintForm Lemmas ElisTarskiPf A Sections NuprlLIB Doc