Nuprl - Proof: s1 1

At: s1 1

1. t: Term

s(t) = SUBX(t; SUBX(f(t); UP(f(t))))

By: Assert (s(t) = SUBX(f(t); f(t)))

Generated subgoals:

1 s(t) = SUBX(f(t); f(t)) 1 step

2 2. s(t) = SUBX(f(t); f(t))
s(t) = SUBX(t; SUBX(f(t); UP(f(t)))) 6 steps

About:

1	`s(t) = SUBX(f(t); f(t))`	1 step

2	2. `s(t) = SUBX(f(t); f(t))` `s(t) = SUBX(t; SUBX(f(t); UP(f(t))))`	6 steps