Nuprl Lemma : bar_26_3a_imp_26_3b
(R: List  . bar_26_3a{i:l}(R))  bar_26_3b{i:l}()
Proof
Definitions occuring in Statement : 
bar_26_3b: bar_26_3b{i:l}(), 
bar_26_3a: bar_26_3a{i:l}(R), 
nat: , 
prop: , 
all: x:A. B[x], 
implies: P  Q, 
function: x:A  B[x]
Definitions : 
so_lambda: x.t[x], 
member: t  T, 
bar_26_1: bar_26_1{i:l}(R), 
bar_26_3b: bar_26_3b{i:l}(), 
prop: , 
implies: P  Q, 
false: False, 
not: A, 
le: A  B, 
nat: , 
all: x:A. B[x], 
so_apply: x[s], 
uall: [x:A]. B[x], 
bar_26_3a: bar_26_3a{i:l}(R), 
guard: {T}
Lemmas : 
bar_26_3a_wf, 
nat_wf, 
Error :list_wf, 
all_wf, 
le_wf, 
equal_wf, 
bar_fwd_fim_wf, 
decidable__equal_nat
(\mforall{}R:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_26\_3a\{i:l\}(R))  {}\mRightarrow{}  bar\_26\_3b\{i:l\}()
Date html generated:
2013_03_20-AM-10_32_06
Last ObjectModification:
2013_03_01-PM-04_54_24
Home
Index