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

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

15. t IN Term & ref(t) = t'
6. r IN Term & ref(r) = r'
SUBX(t; r) IN Term & ref(SUBX(t; r)) = t'/r'		4 steps

About:
equal

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