(7steps total)
PrintForm
Lemmas
ElisTarskiPf
B
Sections
NuprlLIB
Doc
At:
reps
wf
1
1
1
1.
u:
Type
2.
t:
Term
3.
t IN u
4.
x:
u
5.
t IN u
ref(t)
u
By:
BackThru Thm*
a:Term, A:Type. a IN A
ref(a)
A
Generated subgoals:
None
About:
(7steps total)
PrintForm
Lemmas
ElisTarskiPf
B
Sections
NuprlLIB
Doc
ref(t) 
u
a:Term, A:Type. a IN A 
ref(a) A
