Nuprl - Proof: s1 1 2 1 1

At: s1 1 2 1 1

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

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

By: Repeat (ComputeOpid `term_subst` 2)

Generated subgoal:

1 2. s(t) = SUBX((t)[f(t)/X]; SUBX(f(t); UP(f(t))))
s(t) = SUBX(t; SUBX(f(t); UP(f(t)))) 3 steps

About: