{ 
[A:Type]. [B:A 
Type]. [f:x:A fp-> B[x]]. uiff(
fpf-is-empty(f);f = 
) }
{ Proof }
Definitions occuring in Statement :
fpf-is-empty: fpf-is-empty(f),
fpf-empty: ,
fpf: a:A fp-> B[a],
assert: b,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
so_apply: x[s],
function: x:A B[x],
universe: Type,
equal: s = t
Definitions :
fpf: a:A fp-> B[a],
fpf-is-empty: fpf-is-empty(f),
fpf-empty: ,
pi1: fst(t),
member: t 
T,
uall: [x:A]. B[x],
so_apply: x[s],
uiff: uiff(P;Q),
and: P 
Q,
uimplies: b supposing a,
prop: 
,
so_lambda: 
x.t[x],
false: False,
assert: b,
eq_int: (i =
j),
length: ||as||,
top: Top,
all: x:A. B[x],
subtype: S 
T,
ycomb: Y,
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
implies: P 
Q,
iff: P 
Q,
l_member: (x l),
exists: 
x:A. B[x],
nat: 
,
cand: A c B,
le: A 
B,
not: 
A,
pi2: snd(t)
Lemmas :
eq_int_wf,
length_wf1,
assert_wf,
assert_witness,
fpf_wf,
fpf-empty_wf,
iff_weakening_uiff,
assert_of_eq_int,
length_zero,
l_member_wf,
false_wf,
it_wf,
unit_wf,
pi2_wf,
pi1_wf_top
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[f:x:A fp-> B[x]]. uiff(\muparrow{}fpf-is-empty(f);f = \motimes{})
Date html generated:
2011_08_10-AM-07_55_25
Last ObjectModification:
2011_06_18-AM-08_16_38
Home
Index