{ 
[C,B,A:Type]. [a:A]. [u:B 
(C List)].
(interleave1(a;u) 
(A B C) List) }
{ Proof }
Definitions occuring in Statement :
interleave1: interleave1(a;u),
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
interleave1: interleave1(a;u),
so_lambda: 
x.t[x],
top: Top,
all: x:A. B[x],
subtype: S 
T,
so_apply: x[s]
Lemmas :
map_wf,
pi2_wf,
pi1_wf_top
\mforall{}[C,B,A:Type]. \mforall{}[a:A]. \mforall{}[u:B \mtimes{} (C List)]. (interleave1(a;u) \mmember{} (A \mtimes{} B \mtimes{} C) List)
Date html generated:
2011_08_17-PM-07_00_16
Last ObjectModification:
2011_06_18-PM-12_39_55
Home
Index