Nuprl Lemma : rsc2_init_wf

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


Proof not projected



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


Date html generated: 2012_02_20-PM-04_41_56
Last ObjectModification: 2012_02_02-PM-02_05_33

Home Index