{ 
[A,B:Type].  (dataflow(A;B) 
 Type) }
{ Proof }
Definitions occuring in Statement : 
dataflow: dataflow(A;B), 
uall:
[x:A]. B[x], 
member: t 
 T, 
universe: Type
Definitions : 
uall:
[x:A]. B[x], 
member: t 
 T, 
dataflow: dataflow(A;B), 
so_lambda: 
x.t[x], 
so_apply: x[s]
Lemmas : 
corec_wf
\mforall{}[A,B:Type].    (dataflow(A;B)  \mmember{}  Type)
Date html generated:
2011_08_10-AM-08_13_26
Last ObjectModification:
2011_06_18-AM-08_29_16
Home
Index