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

At: qsubx repst 1 1 1
1. t: Term
2. r: Term
3. t': Term
4. r': Term
5. t Term & t = t'
6. r Term & r = r'
SUBX(t; r) Term & SUBX(t; r) = SUBX(t'; r')
By: OnHyps [6;5;0] Analyze
Generated subgoals:

15. t Term
6. t = t'
7. r Term
8. r = r'
SUBX(t; r) Term		1 step
 
25. t Term
6. t = t'
7. r Term
8. r = r'
9. SUBX(t; r) Term
SUBX(t; r) = SUBX(t'; r')		2 steps

About:
equal

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