{ 
[A:Type]. [B:A 
Type]. [eq:EqDecider(A)]. [q:(a:A 
B[a]) List].
[st:a:A fp-> B[a]].
(pi-add(eq;q;st) 
a:A fp-> B[a]) }
{ Proof }
Definitions occuring in Statement :
pi-add: pi-add(eq;q;st),
fpf: a:A fp-> B[a],
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
product: x:A B[x],
list: type List,
universe: Type,
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
pi-add: pi-add(eq;q;st),
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
top: Top,
all: x:A. B[x],
subtype: S 
T,
so_apply: x[s1;s2]
Lemmas :
list_accum_wf,
fpf-join_wf,
fpf-single_wf,
pi1_wf_top,
pi2_wf,
fpf_wf,
deq_wf
\mforall{}[A:Type]. \mforall{}[B:A {}\mrightarrow{} Type]. \mforall{}[eq:EqDecider(A)]. \mforall{}[q:(a:A \mtimes{} B[a]) List]. \mforall{}[st:a:A fp-> B[a]].
(pi-add(eq;q;st) \mmember{} a:A fp-> B[a])
Date html generated:
2011_08_17-PM-07_00_46
Last ObjectModification:
2011_06_18-PM-12_40_45
Home
Index