Nuprl Lemma : ohc_v1_init_wf
ohc_v1_init() 
A:
'. (A 
Id bag(A))
Proof not projected
Definitions occuring in Statement :
ohc_v1_init: ohc_v1_init(),
Id: Id,
member: t T,
isect: x:A. B[x],
function: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
member: t T,
ohc_v1_init: ohc_v1_init(),
all: 
x:A. B[x]
Lemmas :
single-bag_wf,
Id_wf
ohc\_v1\_init() \mmember{} \mcap{}A:\mBbbU{}'. (A {}\mrightarrow{} Id {}\mrightarrow{} bag(A))
Date html generated:
2012_02_20-PM-05_20_56
Last ObjectModification:
2012_02_13-PM-01_05_53
Home
Index