Nuprl Lemma : rsc3_init_wf

rsc3_init()  A:'. (A  Id  bag(A))


Proof not projected



Definitions occuring in Statement :  rsc3_init: rsc3_init(),  Id: Id,  member: t  T,  isect: x:A. B[x],  function: x:A  B[x],  universe: Type,  bag: bag(T)
Definitions :  rsc3_init: rsc3_init(),  member: t  T,  all: x:A. B[x]
Lemmas :  Id_wf,  single-bag_wf
rsc3\_init()  \mmember{}  \mcap{}A:\mBbbU{}'.  (A  {}\mrightarrow{}  Id  {}\mrightarrow{}  bag(A))


Date html generated: 2012_02_20-PM-04_11_45
Last ObjectModification: 2012_02_02-PM-02_03_20

Home Index