Nuprl Lemma : make-lg_wf
[T:Type]. [L:T List]. (make-lg(L) 
LabeledGraph(T))
Proof not projected
Definitions occuring in Statement :
make-lg: make-lg(L),
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
member: t T,
list: type List,
universe: Type
Definitions :
make-lg: make-lg(L),
labeled-graph: LabeledGraph(T),
member: t T,
uall: [x:A]. B[x],
top: Top,
subtype: S 
T,
all: x:A. B[x]
Lemmas :
top_wf,
map_wf,
length_wf,
int_seg_wf,
length-map-sq
\mforall{}[T:Type]. \mforall{}[L:T List]. (make-lg(L) \mmember{} LabeledGraph(T))
Date html generated:
2012_01_23-PM-12_37_18
Last ObjectModification:
2011_12_14-PM-11_07_53
Home
Index