Nuprl Lemma : l_eqset_wf
[T:Type]. [L1,L2:T List]. (l_eqset(T;L1;L2) 
)
Proof not projected
Definitions occuring in Statement :
l_eqset: l_eqset(T;L1;L2),
uall: [x:A]. B[x],
prop: ,
member: t T,
list: type List,
universe: Type
Lemmas :
l_member_wf,
iff_wf
\mforall{}[T:Type]. \mforall{}[L1,L2:T List]. (l\_eqset(T;L1;L2) \mmember{} \mBbbP{})
Date html generated:
2012_02_20-PM-05_55_18
Last ObjectModification:
2012_02_02-PM-02_29_29
Home
Index