{ 
[A:Type]. eq,P:Top. (y
dom(
). w=(y) 
P[y;w] 
True) }
{ Proof }
Definitions occuring in Statement :
fpf-all: xdom(f). v=f(x) P[x; v],
fpf-empty: ,
uall: [x:A]. B[x],
top: Top,
so_apply: x[s1;s2],
all: x:A. B[x],
iff: P Q,
true: True,
universe: Type
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
fpf-all: xdom(f). v=f(x) P[x; v],
fpf-empty: ,
assert: 
b,
fpf-dom: x dom(f),
deq-member: deq-member(eq;x;L),
pi1: fst(t),
reduce: reduce(f;k;as),
bfalse: ff,
ifthenelse: if b then t else f fi ,
member: t T,
iff: P Q,
implies: P Q,
false: False,
true: True,
and: P 
Q,
rev_implies: P Q,
prop: 
Lemmas :
top_wf,
false_wf,
true_wf
\mforall{}[A:Type]. \mforall{}eq,P:Top. (\mforall{}y\mmember{}dom(\motimes{}). w=\motimes{}(y) {}\mRightarrow{} P[y;w] \mLeftarrow{}{}\mRightarrow{} True)
Date html generated:
2011_08_10-AM-08_07_23
Last ObjectModification:
2011_06_18-AM-08_25_16
Home
Index