---

{ [A:Type]
    eq:EqDecider(A). L1,L2:A List. x:A.
      ((x  l_intersection(eq;L1;L2))  (x  L1)  (x  L2)) }

{ Proof }

---

Definitions occuring in Statement :  l_intersection: l_intersection(eq;L1;L2),  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  and: P  Q,  list: type List,  universe: Type,  l_member: (x  l),  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  l_intersection: l_intersection(eq;L1;L2),  and: P  Q,  member: t  T,  prop: ,  iff: P  Q,  rev_implies: P  Q,  implies: P  Q
Lemmas :  deq_wf,  l_member_wf,  filter_wf,  deq-member_wf,  assert_wf,  iff_functionality_wrt_iff,  member_filter,  and_functionality_wrt_iff,  assert-deq-member

---

\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A).  \mforall{}L1,L2:A  List.  \mforall{}x:A.    ((x  \mmember{}  l\_intersection(eq;L1;L2))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L1)  \mwedge{}  (x  \mmember{}  L2))


Date html generated: 2011_08_10-AM-07_48_56
Last ObjectModification: 2011_06_18-AM-08_13_17

Home Index