{ 
[T:Type]. (LabeledGraph(T) 
Type) }
{ Proof }
Definitions occuring in Statement :
labeled-graph: LabeledGraph(T),
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
labeled-graph: LabeledGraph(T),
so_lambda: 
x.t[x],
all: x:A. B[x],
so_apply: x[s]
Lemmas :
Error :dep-isect-wf,
top_wf,
int_seg_wf,
length_wf1
\mforall{}[T:Type]. (LabeledGraph(T) \mmember{} Type)
Date html generated:
2011_08_16-PM-06_35_15
Last ObjectModification:
2011_06_20-AM-01_54_23
Home
Index