Nuprl - Proof: s1 1 2 1 1 1

At: s1 1 2 1 1 1

1. t: Term
2. s(t) = SUBX(q(t)[q(f(t))/X]; SUBX(q(f(t)); Q(q(f(t)))))

s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))

By: Assert (q(t)[q(f(t))/X] = q(t))

Generated subgoals:

1 q(t)[q(f(t))/X] = q(t) 1 step

2 3. q(t)[q(f(t))/X] = q(t)
s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t))))) 1 step

About:

1	`q(t)[q(f(t))/X] = q(t)`	1 step

2	3. `q(t)[q(f(t))/X] = q(t)` `s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))`	1 step