Nuprl Lemma : sm-response_wf
[R:Type]. (sm-response(R) 
Type)
Proof not projected
Definitions occuring in Statement :
sm-response: sm-response(R),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
member: t T,
int: 
,
product: x:A 
B[x],
equal: s = t,
function: x:A 
B[x],
all: x:A. B[x],
Id: Id,
universe: Type,
sm-response: sm-response(R),
axiom: Ax,
isect: 
x:A. B[x],
uall: [x:A]. B[x]
Lemmas :
Id_wf
\mforall{}[R:Type]. (sm-response(R) \mmember{} Type)
Date html generated:
2011_10_20-PM-04_07_56
Last ObjectModification:
2011_01_24-PM-04_56_29
Home
Index