Nuprl Lemma : list-in-fin_spr

Nuprl Lemma : list-in-fin_spr_wf

[B:

List

].

[a:

List]. ((a

fspr(B))

)

Proof

Definitions occuring in Statement : list-in-fin_spr: (a

fspr(B)), bool:

, nat:

, uall:

[x:A]. B[x], member: t

T, function: x:A

B[x]
Definitions : uall:

[x:A]. B[x], nat:

, member: t

T, list-in-fin_spr: (a

fspr(B)), btrue: tt, band: p

q, all:

x:A. B[x], implies: P

Q, ifthenelse: if b then t else f fi , bfalse: ff, so_lambda:

x.t[x], bool:

, unit: Unit, uimplies: b supposing a, uiff: uiff(P;Q), and: P

Q, so_apply: x[s], it:

Lemmas : Error :list_ind_reverse_wf, bool_wf, btrue_wf, eqtt_to_assert, le_int_wf, subtype_rel_set_simple, le_wf, Error :list_wf, nat_wf
\mforall{}[B:\mBbbN{} List {}\mrightarrow{} \mBbbN{}]. \mforall{}[a:\mBbbN{} List]. ((a \mmember{} fspr(B)) \mmember{} \mBbbB{}) Date html generated: 2013_03_20-AM-10_35_00 Last ObjectModification: 2013_03_09-PM-08_54_18 Home Index