Nuprl - Proof: qsubx repst 1

At: qsubx repst 1

1. t: Term
2. r: Term
3. t': Term
4. r': Term
5. t reps t'
6. r reps r'

SUBX(t; r) reps t'/r'

By: OnHyps [0;5;6] (Unfold `repst`)

Generated subgoal:

1 5. t reps t' Term
6. r reps r' Term
SUBX(t; r) reps t'/r' Term 5 steps