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

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

15. t = t'
6. r = r'
SUBX(t; r) = SUBX(t'; r')		5 steps

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