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

At: s2 1 1 2
1. t: Term
SUBX(q(f(t)); Q(q(f(t)))) reps f(t)/q(f(t))
By: BackThru Thm* t,r,t',r':Term. t reps t' & r reps r' SUBX(t; r) reps t'/r'
Generated subgoal:

1 q(f(t)) reps f(t) & Q(q(f(t))) reps q(f(t))3 steps

About:
impliesandall

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