Nuprl Lemma : sm-command_wf
Op:Type. (sm-command(Op) 
Type)
Proof not projected
Definitions occuring in Statement :
sm-command: sm-command(Op),
all: 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-command: sm-command(Op)
Lemmas :
Id_wf
\mforall{}Op:Type. (sm-command(Op) \mmember{} Type)
Date html generated:
2011_10_20-PM-04_06_41
Last ObjectModification:
2011_01_24-PM-04_53_53
Home
Index