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

At: s1 1
1. t: Term
s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))
By: Assert (s(t) = f(t)/q(f(t)))
Generated subgoals:

1 s(t) = f(t)/q(f(t))1 step
 
22. s(t) = f(t)/q(f(t))
s(t) = SUBX(q(t); SUBX(q(f(t)); Q(q(f(t)))))		6 steps

About:
equal

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