(5steps total)
PrintForm
Definitions
ElisTarskiPf
B
Sections
NuprlLIB
Doc
At:
ReflectsProp
wf
P:(Term
Prop), qP:Term, L:(Term
Prop). ReflectsProp(P; qP; L)
Prop
By:
GenUnivCD
Generated subgoals:
1
1.
P:
Term
Prop
2.
qP:
Term
3.
L:
Term
Prop
ReflectsProp(P; qP; L)
Prop
1
step
 
2
1.
P:
Term
Prop{i}
2.
qP:
Term
Term
Prop{i}
Type{i'}
Auto
 
3
1.
P:
Term
Prop
Term
Type
Auto
 
4
Term
Prop{i}
Type{i'}
Auto
About:
(5steps total)
PrintForm
Definitions
ElisTarskiPf
B
Sections
NuprlLIB
Doc