Nuprl - Proof: s1

At: s1

t:Term. s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))

By: GenUnivCD

Generated subgoal:

1 1. t: Term
s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t))))) 8 steps

About: