(8steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: s2 1
1. t: Term
s(t) reps t/(f(t)/q(f(t)))
By: Rewrite Thm* t:Term. s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t))))) 0
Generated subgoal:

1 SUBX(q(t); SUBX(q(f(t)); Q(q(f(t))))) reps t/(f(t)/q(f(t)))6 steps

About:
equalall

(8steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc