Nuprl Lemma : l_disjoint_intersection_implies

[T:Type]. ∀[eq:EqDecider(T)]. ∀[a,b:T List].  l_disjoint(T;a;b) supposing l_disjoint(T;a;l_intersection(eq;a;b))


Proof




Definitions occuring in Statement :  l_intersection: l_intersection(eq;L1;L2) l_disjoint: l_disjoint(T;l1;l2) list: List deq: EqDecider(T) uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a l_disjoint: l_disjoint(T;l1;l2) all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q cand: c∧ B iff: ⇐⇒ Q rev_implies:  Q false: False prop:
Lemmas referenced :  member-intersection and_wf l_member_wf l_disjoint_wf l_intersection_wf list_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution lambdaFormation hypothesis dependent_functionElimination thin hypothesisEquality independent_functionElimination productElimination independent_pairFormation lemma_by_obid isectElimination because_Cache voidElimination sqequalRule lambdaEquality isect_memberEquality equalityTransitivity equalitySymmetry universeEquality

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



Date html generated: 2016_05_14-PM-03_32_46
Last ObjectModification: 2015_12_26-PM-06_01_09

Theory : decidable!equality


Home Index