---

{ [T:Type]. [eq:EqDecider(T)]. [a,b:T List].
    uiff(l_disjoint(T;a;b);l_intersection(eq;a;b) = []) }

{ Proof }

---

Definitions occuring in Statement :  l_intersection: l_intersection(eq;L1;L2),  uiff: uiff(P;Q),  uall: [x:A]. B[x],  nil: [],  list: type List,  universe: Type,  equal: s = t,  l_disjoint: l_disjoint(T;l1;l2),  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  uiff: uiff(P;Q),  l_disjoint: l_disjoint(T;l1;l2),  all: x:A. B[x],  not: A,  and: P  Q,  member: t  T,  uimplies: b supposing a,  prop: ,  implies: P  Q,  false: False,  or: P  Q,  iff: P  Q,  rev_implies: P  Q
Lemmas :  not_wf,  l_member_wf,  l_intersection_wf,  deq_wf,  cons_member,  member-intersection,  nil_member

---

\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a,b:T  List].    uiff(l\_disjoint(T;a;b);l\_intersection(eq;a;b)  =  [])


Date html generated: 2011_08_10-AM-07_49_07
Last ObjectModification: 2011_06_18-AM-08_13_24

Home Index