Nuprl Lemma : fun_exp_set_l_member
L:Id List. i:Id. s:{i:Id| (i 
L)} 
{i:Id| (i L)} . ((i L) 
(n:
. (s^n i L)))
Proof not projected
Definitions occuring in Statement :
Id: Id,
nat: ,
all: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A B[x],
list: type List,
l_member: (x l),
fun_exp: f^n
Lemmas :
decidable__equal_Id,
decidable__l_member,
sq_stable_from_decidable,
fun_exp_add1-sq,
fun_exp_wf,
squash_wf,
true_wf,
rev_implies_wf,
iff_wf,
nat_ind_tp,
l_member_wf,
Id_wf,
nat_wf,
member_wf,
not_wf,
false_wf,
le_wf,
nat_properties,
ge_wf
\mforall{}L:Id List. \mforall{}i:Id. \mforall{}s:\{i:Id| (i \mmember{} L)\} {}\mrightarrow{} \{i:Id| (i \mmember{} L)\} . ((i \mmember{} L) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (s\^{}n i \mmember{} L)))
Date html generated:
2012_02_20-PM-05_55_06
Last ObjectModification:
2012_02_02-PM-02_29_23
Home
Index