{ 
[A:Type]. [eq:EqDecider(A)]. [f:a:A fp-> Top]. [L:A List].
uiff(l_disjoint(A;fst(f);L);[a:A]. 
(a 
L) supposing 
a dom(f)) }
{ Proof }
Definitions occuring in Statement :
fpf-dom: x dom(f),
fpf: a:A fp-> B[a],
assert: b,
uiff: uiff(P;Q),
uimplies: b supposing a,
uall: [x:A]. B[x],
top: Top,
pi1: fst(t),
not: A,
list: type List,
universe: Type,
l_disjoint: l_disjoint(T;l1;l2),
l_member: (x l),
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
fpf: a:A fp-> B[a],
top: Top,
uiff: uiff(P;Q),
l_disjoint: l_disjoint(T;l1;l2),
uimplies: b supposing a,
fpf-dom: x dom(f),
not: A,
all: x:A. B[x],
and: P 
Q,
member: t T,
implies: P 
Q,
false: False,
prop: 
,
subtype: S 
T,
so_lambda: 
x.t[x],
so_apply: x[s],
iff: P 
Q,
rev_implies: P Q
Lemmas :
l_member_wf,
assert_wf,
deq-member_wf,
pi1_wf_top,
top_wf,
not_wf,
uall_wf,
deq_wf,
assert-deq-member
\mforall{}[A:Type]. \mforall{}[eq:EqDecider(A)]. \mforall{}[f:a:A fp-> Top]. \mforall{}[L:A List].
uiff(l\_disjoint(A;fst(f);L);\mforall{}[a:A]. \mneg{}(a \mmember{} L) supposing \muparrow{}a \mmember{} dom(f))
Date html generated:
2011_08_10-AM-08_11_16
Last ObjectModification:
2011_06_18-AM-08_26_48
Home
Index