Nuprl Lemma : leaders-finite_wf
[l:
Id]. (Finitely many leaders 
)
Proof not projected
Definitions occuring in Statement :
leaders-finite: Finitely many leaders,
Id: Id,
nat: ,
uall: [x:A]. B[x],
prop: ,
member: t T,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
member: t T,
prop: ,
leaders-finite: Finitely many leaders,
exists: 
x:A. B[x],
and: P 
Q,
all: x:A. B[x],
so_lambda: 
x.t[x],
so_apply: x[s]
Lemmas :
Id_wf,
nat_wf,
l_member_wf,
l_all_wf2
\mforall{}[l:\mBbbN{} {}\mrightarrow{} Id]. (Finitely many leaders \mmember{} \mBbbP{})
Date html generated:
2011_10_20-PM-04_42_10
Last ObjectModification:
2011_06_18-PM-02_08_20
Home
Index