Nuprl Lemma : l-union-left-contains

[T:Type]. ∀eq:EqDecider(T). ∀as,bs,cs:T List.  (as ⊆ bs  as ⊆ bs ⋃ cs)


Proof




Definitions occuring in Statement :  l-union: as ⋃ bs l_contains: A ⊆ B list: List deq: EqDecider(T) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q l_contains: A ⊆ B member: t ∈ T so_lambda: λ2x.t[x] prop: so_apply: x[s] iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q l_member: (x ∈ l) exists: x:A. B[x] or: P ∨ Q guard: {T} nat: int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B l_all: (∀x∈L.P[x]) cand: c∧ B
Lemmas referenced :  l_all_iff l_member_wf l-union_wf member-union all_wf or_wf l_contains_wf list_wf deq_wf lelt_wf length_wf and_wf equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality dependent_functionElimination sqequalRule lambdaEquality cumulativity setElimination rename hypothesis setEquality productElimination independent_functionElimination inlFormation because_Cache addLevel allFunctionality impliesFunctionality functionEquality universeEquality dependent_set_memberEquality independent_pairFormation hyp_replacement equalitySymmetry levelHypothesis equalityTransitivity applyEquality

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}as,bs,cs:T  List.    (as  \msubseteq{}  bs  {}\mRightarrow{}  as  \msubseteq{}  bs  \mcup{}  cs)



Date html generated: 2016_10_21-AM-10_38_27
Last ObjectModification: 2016_07_12-AM-05_49_06

Theory : decidable!equality


Home Index