{ 
[P:Unit 
]. (Dec(P[
]) 
Dec(
x:Unit. P[x])) }
{ Proof }
Definitions occuring in Statement :
decidable: Dec(P),
it: ,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
exists: x:A. B[x],
implies: P Q,
unit: Unit,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
prop: ,
implies: P Q,
so_apply: x[s],
all: x:A. B[x],
member: t 
T,
so_lambda: 
x.t[x],
finite-type: finite-type(T),
exists: x:A. B[x],
nat: 
,
le: A 
B,
not: 
A,
false: False,
surject: Surj(A;B;f),
int_seg: {i..j
},
lelt: i j < k,
and: P 
Q,
unit: Unit,
it:
Lemmas :
decidable-exists-finite,
unit_wf,
decidable_wf,
it_wf,
le_wf,
int_seg_wf,
surject_wf
\mforall{}[P:Unit {}\mrightarrow{} \mBbbP{}]. (Dec(P[\mcdot{}]) {}\mRightarrow{} Dec(\mexists{}x:Unit. P[x]))
Date html generated:
2011_08_16-AM-11_10_54
Last ObjectModification:
2011_06_20-AM-00_19_03
Home
Index