{ 
[A,B:Type]. [x:A]. [v:B]. [eqa:EqDecider(A)].
(x : v 
a:A fp-> x : B(a)?Top) }
{ Proof }
Definitions occuring in Statement :
fpf-single: x : v,
fpf-cap: f(x)?z,
fpf: a:A fp-> B[a],
uall: [x:A]. B[x],
top: Top,
member: t T,
universe: Type,
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
member: t T,
so_lambda: 
x.t[x],
fpf-cap: f(x)?z,
fpf-single: x : v,
fpf-dom: x dom(f),
deq-member: deq-member(eq;x;L),
pi1: fst(t),
reduce: reduce(f;k;as),
ifthenelse: if b then t else f fi ,
bor: p 
q,
btrue: tt,
so_apply: x[s]
Lemmas :
fpf-single_wf,
deq_wf,
ifthenelse_wf,
bor_wf,
eqof_wf,
bfalse_wf,
top_wf,
eqof_eq_btrue,
subtype_rel_self
\mforall{}[A,B:Type]. \mforall{}[x:A]. \mforall{}[v:B]. \mforall{}[eqa:EqDecider(A)]. (x : v \mmember{} a:A fp-> x : B(a)?Top)
Date html generated:
2011_08_10-AM-08_02_37
Last ObjectModification:
2011_06_18-AM-08_20_35
Home
Index