Nuprl Lemma : vr_test_length_ext
[T:Type]. (T List 
)
Proof not projected
Definitions occuring in Statement :
uall: [x:A]. B[x],
function: x:A B[x],
list: type List,
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t 
T
Lemmas :
uall_wf
\mforall{}[T:Type]. (T List {}\mrightarrow{} \mBbbZ{})
Date html generated:
2012_02_20-PM-03_35_49
Last ObjectModification:
2012_02_02-PM-03_29_18
Home
Index