Nuprl Lemma : l_contains_disjoint

[T:Type]. ∀[A,B,C:T List].  (l_disjoint(T;B;C)) supposing (l_disjoint(T;A;C) and B ⊆ A)


Definitions occuring in Statement :  l_disjoint: l_disjoint(T;l1;l2) l_contains: A ⊆ B list: List uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] l_disjoint: l_disjoint(T;l1;l2) l_contains: A ⊆ B uimplies: supposing a member: t ∈ T all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q false: False prop: so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q
Lemmas referenced :  l_member_wf all_wf not_wf l_all_iff l_all_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination independent_pairFormation productElimination promote_hyp voidElimination productEquality extract_by_obid isectElimination because_Cache sqequalRule lambdaEquality isect_memberEquality equalityTransitivity equalitySymmetry functionEquality addLevel independent_isectElimination setElimination rename setEquality cumulativity isectEquality universeEquality

\mforall{}[T:Type].  \mforall{}[A,B,C:T  List].    (l\_disjoint(T;B;C))  supposing  (l\_disjoint(T;A;C)  and  B  \msubseteq{}  A)

Date html generated: 2019_06_20-PM-01_27_01
Last ObjectModification: 2018_08_24-PM-11_15_23

Theory : list_1

Home Index