(7steps total)
PrintForm
Definitions
Lemmas
ElisTarskiPf
B
Sections
NuprlLIB
Doc
At:
reps
wf
1
1.
u:
Type
2.
t:
u Term
3.
x:
u
(t reps x
u)
Prop
By:
Unfold `reps` 0
Generated subgoal:
1
(t IN u & ref(t) = x)
Prop
2
steps
About:
(7steps total)
PrintForm
Definitions
Lemmas
ElisTarskiPf
B
Sections
NuprlLIB
Doc
(t IN u & ref(t) = x) 
Prop
(t reps x u) Prop
(t IN u & ref(t) = x) Prop
