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

At: qsubx repst 1 1 1 2
1. t: Term
2. r: Term
3. t': Term
4. r': Term
5. t IN Term
6. ref(t) = t'
7. r IN Term
8. ref(r) = r'
9. SUBX(t; r) IN Term
ref(SUBX(t; r)) = t'/r'
By: ComputeOpid `down` 0
Generated subgoal:

1 ref(t)/ref(r) = t'/r'1 step

About:
equal

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