(6steps total)
PrintForm
Lemmas
ElisTarskiPf
A
Sections
NuprlLIB
Doc
At:
reps
wf2
1
1
1
1.
t:
Term
2.
x:
Term
3.
t
Term
is_subst0(.(
t))
By:
FwdThru Thm*
a:Term, A:Type. a
A
a
A [3]
Generated subgoals:
None
About:
(6steps total)
PrintForm
Lemmas
ElisTarskiPf
A
Sections
NuprlLIB
Doc
Term
is_subst0(.(t))
a:Term, A:Type. a A 
a A [3]