{ 
[A:Type]. [eq:EqDecider(A)]. [L1,L2:A List].
(l_intersection(eq;L1;L2) 
A List) }
{ Proof }
Definitions occuring in Statement :
l_intersection: l_intersection(eq;L1;L2),
uall: [x:A]. B[x],
member: t T,
list: type List,
universe: Type,
deq: EqDecider(T)
Definitions :
uall: [x:A]. B[x],
member: t T,
l_intersection: l_intersection(eq;L1;L2)
Lemmas :
filter_wf,
deq-member_wf,
deq_wf
\mforall{}[A:Type]. \mforall{}[eq:EqDecider(A)]. \mforall{}[L1,L2:A List]. (l\_intersection(eq;L1;L2) \mmember{} A List)
Date html generated:
2011_08_10-AM-07_48_53
Last ObjectModification:
2011_06_18-AM-08_13_15
Home
Index