{ 
[A,B:Type]. (ThresholdComb2(A;B) 
CombinatorDef) }
{ Proof }
Definitions occuring in Statement :
ThresholdComb2: ThresholdComb2(A;B),
combinator-def: CombinatorDef,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
ThresholdComb2: ThresholdComb2(A;B),
top: Top,
all: x:A. B[x],
subtype: S 
T
Lemmas :
MapFilterComb_wf,
unit_wf,
threshold_val_wf,
top_wf
\mforall{}[A,B:Type]. (ThresholdComb2(A;B) \mmember{} CombinatorDef)
Date html generated:
2011_08_17-PM-06_30_25
Last ObjectModification:
2010_11_12-AM-08_52_01
Home
Index