Nuprl - Proof: qsubx repst 1 1 1 2 1

At: qsubx repst 1 1 1 2 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'
9. SUBX(t; r) Term

SUBX(t; r) = SUBX(t'; r')

By: HypSubst 6 0 THEN HypSubst 8 0

Generated subgoals:

None

About: