Nuprl - Proof: qsubx repst 1 1

At: qsubx repst 1 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 `reps`)

Generated subgoal:

1 5. t Term & t = t'
6. r Term & r = r'
SUBX(t; r) Term & SUBX(t; r) = SUBX(t'; r') 4 steps

About: